On 14/05/2013 10:10 PM, Orchid Win7 v1 wrote:
>
>    "What part of
>
>      x : σ ∈ Γ
>      ----------
>      Γ ⊢ x : σ
>
>
>      Γ ⊢ e0 : τ → τ',  Γ ⊢ e1 : τ
>      -----------------------------
>             Γ ⊢ e0 e1 : τ'
>
>
>       Γ, x : τ ⊢ e : τ'
>      --------------------
>      Γ ⊢ λ x . e : τ → τ'
>
>
>      Γ ⊢ e0 : σ,  Γ, x : σ ⊢ e1 : τ
>      -------------------------------
>        Γ ⊢ let x = e0 in e1 : τ
>
>
>      Γ ⊢ e : σ',  σ' ⊑ σ
>      --------------------
>           Γ ⊢ e : σ
>
>
>      Γ ⊢ e : σ,  α ∉ free(Γ)
>      -------------------------
>      Γ ⊢ e : ∀ α . σ
>
>    do you NOT understand?"

Love it.

I want it on a tee-shirt.

-- 
Regards
     Stephen

Post a reply to this message