inductive Typing : List Ty → Term → Ty → Prop

• var {Γ : List Ty} {T : Ty} {x : Nat} : Γ[x]? = some T → Γ ⊢ #x : T
• app {Γ : List Ty} {A B : Ty} {f a : Term} : Γ ⊢ f : (A -t> B) → Γ ⊢ a : A → Γ ⊢ (f :@ a) : B
• lam {Γ : List Ty} {A B : Ty} {t : Term} : (A :: Γ) ⊢ t : B → Γ ⊢ :λ[A] t : (A -t> B)

def «term_⊢_:_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem typing_renaming_lift {Γ Δ : List Ty} (A : Ty) {r : LeanSubst.Ren} : (∀ (x : Nat) (T : Ty), Γ ⊢ #x : T → Δ ⊢ #(r x) : T) → ∀ (x : Nat) (T : Ty), (A :: Γ) ⊢ #x : T → (A :: Δ) ⊢ #(r.lift x) : T

theorem typing_weaken {Γ : List Ty} {t : Term} {A : Ty} (Δ : List Ty) (r : LeanSubst.Ren) : Γ ⊢ t : A → (∀ (x : Nat) (T : Ty), Γ ⊢ #x : T → Δ ⊢ #(r x) : T) → Δ ⊢ r.apply t : A

theorem typing_subst_lift {Γ Δ : List Ty} (A : Ty) {σ : LeanSubst.Subst Term} : (∀ (x : Nat) (T : Ty), Γ ⊢ #x : T → Δ ⊢ ↑(σ x) : T) → ∀ (x : Nat) (T : Ty), (A :: Γ) ⊢ #x : T → (A :: Δ) ⊢ ↑(σ.lift x) : T

theorem typing_subst {Γ : List Ty} {t : Term} {A : Ty} (Δ : List Ty) (σ : LeanSubst.Subst Term) : Γ ⊢ t : A → (∀ (x : Nat) (T : Ty), Γ ⊢ #x : T → Δ ⊢ ↑(σ x) : T) → Δ ⊢ t[σ] : A

theorem typing_beta {Γ : List Ty} {A B : Ty} {b t : Term} : (A :: Γ) ⊢ b : B → Γ ⊢ t : A → Γ ⊢ b[%t::LeanSubst.I] : B