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

• (Term.var 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 }

instance instPrefixHash_Term : LeanSubst.PrefixHash Term

Equations

• instPrefixHash_Term = { hash := Term.var }

@[simp]

theorem Term.var_def {x : Nat} : var x = #x

@[simp]

theorem Term.var_eq {x y : Nat} : (#x = #y) = (x = y)

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 smap (lf : LeanSubst.Subst.Lift Term) (f : Nat → LeanSubst.Subst.Action Term) : Term → Term

Equations

• smap lf f (Term.var x) = match f x with | LeanSubst.Subst.Action.re y => #y | LeanSubst.Subst.Action.su t => t
• smap lf f (f_1 :@ a_1) = smap lf f f_1 :@ smap lf f a_1
• smap lf f (:λ[a_1] t) = :λ[a_1] smap lf (lf f) t

instance SubstMap_Term : LeanSubst.SubstMap Term

Equations

• SubstMap_Term = { smap := smap }

instance HasSimpleVar_Term : LeanSubst.HasSimpleVar Term

Equations

• HasSimpleVar_Term = { var := Term.var, smap := @HasSimpleVar_Term._proof_1 }

@[simp]

theorem subst_var {x : Nat} {σ : LeanSubst.Subst Term} : #x[σ] = match σ x with | LeanSubst.Subst.Action.re y => #y | LeanSubst.Subst.Action.su t => t

@[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]

theorem apply_id {t : Term} : t[LeanSubst.I] = t

theorem apply_stable {r : LeanSubst.Ren} {σ : LeanSubst.Subst Term} : r.to = σ → 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)

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

Equations

• ↑(LeanSubst.Subst.Action.su t) = t
• ↑(LeanSubst.Subst.Action.re k) = #k

def «term↑_» : Lean.ParserDescr

Equations

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