def Ty.decEq (a b : Ty) : Decidable (a = b)

Equations

• One or more equations did not get rendered due to their size.
• ⊤.decEq ⊤ = isTrue ⋯
• ⊤.decEq (a -t> a_1) = isFalse ⋯
• (a -t> a_1).decEq ⊤ = isFalse ⋯

instance instInhabitedTy : Inhabited Ty

Equations

• instInhabitedTy = { default := ⊤ }

instance instDecidableEqTy : DecidableEq Ty

Equations

• instDecidableEqTy = Ty.decEq

def is_arrow : Ty → Option (Ty × Ty)

Equations

• is_arrow ⊤ = none
• is_arrow (A -t> B) = some (A, B)

def infer (Γ : List Ty) : Term → Option Ty

Equations

• infer Γ (Term.var x_1) = Γ[x_1]?
• infer Γ (f :@ a) = do let T ← infer Γ f let A' ← infer Γ a let __discr ← is_arrow T match __discr with | (A, B) => if A = A' then some B else none
• infer Γ (:λ[A] t) = do let B ← infer (A :: Γ) t pure (A -t> B)

theorem infer_sound {Γ : List Ty} {t : Term} {A : Ty} : infer Γ t = some A → Γ ⊢ t : A