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: 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

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

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) = λ[x // a] a_1
• ([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).fv = a.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 : Trm) (s : Trm) (y : ℕ) (h : y ∉ t.fv) : ([y // s] t) = t