• MasterMason #9
    Már értem, most megvilágosodtam.

    A <: B
    ∆, x : A ⊲ x : B
    (ax 1)
    !Ac <: B
    ∆ ⊲ c : B
    (ax 2)
    ∆ ⊲ M : !
    n
    A
    ∆ ⊲ inj
    l
    (M) : !
    n
    (A ⊕ B)
    (⊕.I1)
    ∆ ⊲ N : !
    n
    B
    ∆ ⊲ inj
    r
    (N) : !
    n
    (A ⊕ B)
    (⊕.I2)
    !∆, Γ1 ⊲ P : !
    n
    (A ⊕ B)
    !∆, Γ2, x : !
    n
    A ⊲ M : C
    !∆, Γ2, y : !
    n
    B ⊲ N : C
    Γ1, Γ2, !∆ ⊲ match P with (x 7→ M | y 7→ N) : C
    (⊕.E)
    Γ1, !∆ ⊲ M : A⊸ B Γ2, !∆ ⊲ N : A
    Γ1, Γ2, !∆ ⊲ MN : B
    (app)
    x : A,∆ ⊲ M : B
    ∆ ⊲ λx.M : A⊸ B
    (λ1)
    If F V (M) ∩ |Γ| = ∅:
    Γ, !∆, x : A ⊲ M : B
    Γ, !∆ ⊲ λx.M : !
    n+1
    (A ⊸ B)
    (λ2)
    !∆, Γ1 ⊲ M1 : !
    n
    A1 !∆, Γ2 ⊲ M2 : !
    n
    A2
    !∆, Γ1, Γ2 ⊲ hM1, M2i : !
    n
    (A1 ⊗ A2)
    (⊗.I)
    ∆ ⊲ ∗ : !
    n

    (⊤)
    !∆, Γ1 ⊲ M : !
    n
    (A1 ⊗ A2) !∆, Γ2, x1:!
    n
    A1, x2:!
    n
    A2 ⊲ N : A
    !∆, Γ1, Γ2 ⊲ let hx1, x2i = M in N : A
    (⊗.E)
    !∆, f : !(A ⊸ B), x : A ⊲ M : B !∆, Γ, f : !(A⊸ B) ⊲ N : C
    !∆, Γ ⊲ let rec f x = M in N : C