inductive Typ : Type

• typ_base : Typ
• typ_arrow : Typ → Typ → Typ

instance instDecidableEqTyp : DecidableEq Typ

Equations

• instDecidableEqTyp = decEqTyp✝

instance instReprTyp : Repr Typ

Equations

• instReprTyp = { reprPrec := reprTyp✝ }

inductive Trm : Type

• bvar : ℕ → Trm
• fvar : ℕ → Trm
• abs : Typ → Trm → Trm
• app : Trm → Trm → Trm

instance instDecidableEqTrm : DecidableEq Trm

Equations

• instDecidableEqTrm = decEqTrm✝

instance instReprTrm : Repr Trm

Equations

• instReprTrm = { reprPrec := reprTrm✝ }

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

Equations

• Trm.«term_->_» = Lean.ParserDescr.trailingNode `Trm.«term_->_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " -> ") (Lean.ParserDescr.cat `term 0))

def Trm.«term€_» : Lean.ParserDescr

Equations

• Trm.«term€_» = Lean.ParserDescr.node `Trm.«term€_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "€") (Lean.ParserDescr.cat `term 0))

def Trm.«term$_» : Lean.ParserDescr

Equations

• Trm.«term$_» = Lean.ParserDescr.node `Trm.«term$_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "$") (Lean.ParserDescr.cat `term 0))

def Trm.«termλ_,_» : Lean.ParserDescr

Equations

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

def Trm.«term_@_» : Lean.TrailingParserDescr

Equations

• Trm.«term_@_» = Lean.ParserDescr.trailingNode `Trm.«term_@_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " @ ") (Lean.ParserDescr.cat `term 0))

def Trm.subst (x : ℕ) (a : Trm) : Trm → Trm

Equations

• ([x // a] €a_1) = €a_1
• ([x // a] $a_1) = if a_1 = x then a else $a_1
• ([x // a] λ a_1,a_2) = λ a_1,[x // a] a_2
• ([x // a] a_1 @ a_2) = ([x // a] a_1) @ [x // a] a_2

def Trm.«term[_//_]_» : Lean.ParserDescr

Equations

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

def Trm.fv : Trm → Finset ℕ

Equations

• (€a).fv = ∅
• ($a).fv = {a}
• (λ a,a_1).fv = a_1.fv
• (a @ a_1).fv = a.fv ∪ a_1.fv

theorem Trm.pick_fresh (t : Trm) (L : Finset ℕ) : ∃ (x : ℕ), x ∉ L ∪ t.fv

theorem Trm.subst_fresh (t u : Trm) (y : ℕ) (h : y ∉ t.fv) : ([y // u] t) = t