inductive Ty : Type

• base : Ty
• arrow : Ty → Ty → Ty

def «term⊤» : Lean.ParserDescr

Equations

• «term⊤» = Lean.ParserDescr.node `«term⊤» 1024 (Lean.ParserDescr.symbol "⊤")

def «term_-t>_» : Lean.TrailingParserDescr

Equations

• «term_-t>_» = Lean.ParserDescr.trailingNode `«term_-t>_» 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " -t> ") (Lean.ParserDescr.cat `term 40))

def Ty.repr (a : Ty) (p : Nat) : Std.Format

Equations

• ⊤.repr p = Std.Format.text "⊤"
• (⊤ -t> B).repr p = ⊤.repr p ++ Std.Format.text " -> " ++ B.repr p
• (A -t> B).repr p = Std.Format.text "(" ++ A.repr p ++ Std.Format.text ") -> " ++ B.repr p

instance instReprTy : Repr Ty

Equations

• instReprTy = { reprPrec := Ty.repr }

inductive Term : Type

• var : Nat → Term
• app : Term → Term → Term
• lam : Ty → Term → Term

def Term.repr (a : Term) (p : Nat) : Std.Format

Equations

• (#x).repr p = Std.Format.text "#" ++ Std.Format.text x.repr
• (f :@ a_2).repr p = Std.Format.text "(" ++ f.repr p ++ Std.Format.text " " ++ a_2.repr p ++ Std.Format.text ")"
• (:λ[a_2] t).repr p = Std.Format.text "(λ " ++ t.repr p ++ Std.Format.text ")"

instance instReprTerm : Repr Term

Equations

• instReprTerm = { reprPrec := Term.repr }

def «term#_» : Lean.ParserDescr

Equations

• «term#_» = Lean.ParserDescr.node `«term#_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") (Lean.ParserDescr.cat `term 1024))

def «term_:@_» : Lean.TrailingParserDescr

Equations

• «term_:@_» = Lean.ParserDescr.trailingNode `«term_:@_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " :@ ") (Lean.ParserDescr.cat `term 66))

def «term:λ[_]_» : Lean.ParserDescr

Equations

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

def Term.from_action : LeanSubst.Subst.Action Term → Term

Equations

• ↑(LeanSubst.re y) = #y
• ↑(LeanSubst.su t) = t

@[simp]

theorem Term.from_action_id {n : Nat} : ↑(+0 n) = #n

@[simp]

theorem Term.from_action_succ {n : Nat} : ↑(+1 n) = #(n + 1)

@[simp]

theorem Term.from_acton_re {n : Nat} : ↑(LeanSubst.re n) = #n

@[simp]

theorem Term.from_action_su {t : Term} : ↑(LeanSubst.su t) = t

instance instCoe_SubstActionTerm_Term : Coe (LeanSubst.Subst.Action Term) Term

Equations

• instCoe_SubstActionTerm_Term = { coe := Term.from_action }

def smap (k : LeanSubst.Subst.Kind) (lf : LeanSubst.Subst.Lift Term k) (f : LeanSubst.SplitSubst Term k) : Term → Term

Equations

• smap LeanSubst.Subst.Kind.re lf_2 f_2 #x = #(f_2 x)
• smap LeanSubst.Subst.Kind.su lf_2 f_2 #x = ↑(f_2 x)
• smap k lf f (f_1 :@ a_1) = smap k lf f f_1 :@ smap k lf f a_1
• smap k lf f (:λ[a_1] t) = :λ[a_1] smap k lf (lf f) t

instance SubstMap_Term : LeanSubst.SubstMap Term

Equations

• SubstMap_Term = { smap := smap }

@[simp]

theorem subst_var {σ : LeanSubst.Subst Term} {x : Nat} : (#x)[σ] = ↑(σ x)

@[simp]

theorem subst_app {σ : LeanSubst.Subst Term} {t1 t2 : Term} : (t1 :@ t2)[σ] = t1[σ] :@ t2[σ]

@[simp]

theorem subst_lam {σ : LeanSubst.Subst Term} {A : Ty} {t : Term} : (:λ[A] t)[σ] = :λ[A] t[σ.lift]

@[simp]

theorem Term.from_action_compose {x : Nat} {σ τ : LeanSubst.Subst Term} : (↑(σ x))[τ] = ↑((σ ∘ τ) x)

theorem apply_id {t : Term} : t[+0] = t

theorem apply_stable (r : LeanSubst.Ren) (σ : LeanSubst.Subst Term) : ↑r = σ → r.apply = σ.apply

instance SubstMapStable_Term : LeanSubst.SubstMapStable Term

theorem apply_compose {s : Term} {σ τ : LeanSubst.Subst Term} : s[σ][τ] = s[σ ∘ τ]

instance SubstMapCompose_Term : LeanSubst.SubstMapCompose Term

inductive Neutral : Term → Prop

• var {x : Nat} : Neutral #x
• app {f a : Term} : Neutral f → Neutral (f :@ a)

theorem to_ren_is_var {x : Nat} {t : Term} {r : LeanSubst.Ren} : t = ↑(↑r x) → ∃ (y : Nat), t = #y

theorem ren_subst_apply_eq_lift {r : LeanSubst.Ren} {σ : LeanSubst.Subst Term} : (∀ (i x : Nat), r i = x → ↑(σ i) = #x ∨ σ i = LeanSubst.re x) → ∀ (i x : Nat), r.lift i = x → ↑(σ.lift i) = #x ∨ σ.lift i = LeanSubst.re x

theorem ren_subst_apply_eq {t : Term} {r : LeanSubst.Ren} {σ : LeanSubst.Subst Term} : (∀ (i x : Nat), r i = x → ↑(σ i) = #x ∨ σ i = LeanSubst.re x) → t[↑r] = t[σ]