Require Import HaskCoreTypes.
Require Import HaskLiteralsAndTyCons.
Require Import HaskStrongTypes.
Require Import HaskCoreTypes.
Require Import HaskLiteralsAndTyCons.
Require Import HaskStrongTypes.
(* A judgment consists of an environment shape (Γ and Δ) and a pair of trees of leveled types (the antecedent and succedent) valid
* in any context of that shape. Notice that the succedent contains a tree of types rather than a single type; think
(* A judgment consists of an environment shape (Γ and Δ) and a pair of trees of leveled types (the antecedent and succedent) valid
* in any context of that shape. Notice that the succedent contains a tree of types rather than a single type; think
| RLam : forall Γ Δ Σ (tx:HaskType Γ ★) te l, Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l] ] [Γ>Δ> Σ |- [tx--->te @@l]]
| RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->
| RLam : forall Γ Δ Σ (tx:HaskType Γ ★) te l, Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l] ] [Γ>Δ> Σ |- [tx--->te @@l]]
| RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->