inductive SecondOrder.Kind : Type

• star: SecondOrder.Kind

instance SecondOrder.instReprKind : Repr SecondOrder.Kind

Equations

• SecondOrder.instReprKind = { reprPrec := SecondOrder.reprKind✝ }

instance SecondOrder.instDecidableEqKind : DecidableEq SecondOrder.Kind

Equations

• SecondOrder.instDecidableEqKind x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

def SecondOrder.«term∗» : Lean.ParserDescr

Equations

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

instance SecondOrder.instToStringKind : ToString SecondOrder.Kind

Equations

• SecondOrder.instToStringKind = { toString := fun (k : SecondOrder.Kind) => match k with | ∗ => "∗" }

inductive SecondOrder.Typ : Type

• var: Name → SecondOrder.Typ
• arrow: SecondOrder.Typ → SecondOrder.Typ → SecondOrder.Typ
• pi: Name → SecondOrder.Kind → SecondOrder.Typ → SecondOrder.Typ

instance SecondOrder.instReprTyp : Repr SecondOrder.Typ

Equations

• SecondOrder.instReprTyp = { reprPrec := SecondOrder.reprTyp✝ }

instance SecondOrder.instDecidableEqTyp : DecidableEq SecondOrder.Typ

Equations

• SecondOrder.instDecidableEqTyp = SecondOrder.decEqTyp✝

def SecondOrder.Typ.toString : SecondOrder.Typ → String

Equations

• (SecondOrder.Typ.var a).toString = a
• (a ⇒ a_1).toString = toString "" ++ toString a.toString ++ toString " → " ++ toString a_1.toString ++ toString ""
• (Πa:a_1,a_2).toString = toString "Π " ++ toString a ++ toString " : " ++ toString a_1 ++ toString ". " ++ toString a_2.toString ++ toString ""

instance SecondOrder.Typ.instToString : ToString SecondOrder.Typ

Equations

• SecondOrder.Typ.instToString = { toString := SecondOrder.Typ.toString }

instance SecondOrder.Typ.instCoeName : Coe Name SecondOrder.Typ

Equations

• SecondOrder.Typ.instCoeName = { coe := SecondOrder.Typ.var }

def SecondOrder.Typ.«term_⇒_» : Lean.TrailingParserDescr

Equations

• SecondOrder.Typ.«term_⇒_» = Lean.ParserDescr.trailingNode `SecondOrder.Typ.term_⇒_ 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇒ ") (Lean.ParserDescr.cat `term 20))

def SecondOrder.Typ.«termΠ_:_,_» : Lean.ParserDescr

Equations

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

inductive SecondOrder.Term : Type

• var: Name → SecondOrder.Term
• app: SecondOrder.Term → SecondOrder.Term → SecondOrder.Term
• tapp: SecondOrder.Term → SecondOrder.Typ → SecondOrder.Term
• abs: Name → SecondOrder.Typ → SecondOrder.Term → SecondOrder.Term
• tabs: Name → SecondOrder.Kind → SecondOrder.Term → SecondOrder.Term

instance SecondOrder.instReprTerm : Repr SecondOrder.Term

Equations

• SecondOrder.instReprTerm = { reprPrec := SecondOrder.reprTerm✝ }

instance SecondOrder.instDecidableEqTerm : DecidableEq SecondOrder.Term

Equations

• SecondOrder.instDecidableEqTerm = SecondOrder.decEqTerm✝

def SecondOrder.Term.toString : SecondOrder.Term → String

Equations

• (SecondOrder.Term.var a).toString = a
• (a ∙ a_1).toString = toString "(" ++ toString a.toString ++ toString " " ++ toString a_1.toString ++ toString ")"
• (a ∙ₜ a_1).toString = toString "(" ++ toString a.toString ++ toString " [" ++ toString a_1.toString ++ toString "])"
• (SecondOrder.Term.abs a a_1 a_2).toString = toString "(λ" ++ toString a ++ toString " : " ++ toString a_1 ++ toString ". " ++ toString a_2.toString ++ toString ")"
• (Λ a:a_1,a_2).toString = toString "(Λ" ++ toString a ++ toString " : " ++ toString a_1 ++ toString ". " ++ toString a_2.toString ++ toString ")"

instance SecondOrder.Term.instToString : ToString SecondOrder.Term

Equations

• SecondOrder.Term.instToString = { toString := SecondOrder.Term.toString }

instance SecondOrder.Term.instCoeName : Coe Name SecondOrder.Term

Equations

• SecondOrder.Term.instCoeName = { coe := SecondOrder.Term.var }

def SecondOrder.Term.«term_∙_» : Lean.TrailingParserDescr

Equations

• SecondOrder.Term.«term_∙_» = Lean.ParserDescr.trailingNode `SecondOrder.Term.term_∙_ 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∙ ") (Lean.ParserDescr.cat `term 101))

def SecondOrder.Term.«term_∙ₜ_» : Lean.TrailingParserDescr

Equations

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

def SecondOrder.Term.«termΛ_:_,_» : Lean.ParserDescr

Equations

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