def Paper.«command_Paper_link[_]__» : Lean.ParserDescr

Equations

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

def Paper.«command_Paper_thm[_]__» : Lean.ParserDescr

Equations

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

def Paper.Link {α : Sort u_1} : α → Prop

Equations

• Paper.Link x✝ = True

def Paper.LinkThm (α : Sort u_1) : {x : α} → Prop

Equations

• Paper.LinkThm α = True

def Paper.LinkLem (α : Sort u_1) : {x : α} → Prop

Equations

• Paper.LinkLem α = True

axiom Paper.paperAx {α : Sort u_1} : α

def Paper.pkind.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.pkind : Category

Equations

• Lean.Parser.Category.pkind = { }

def Paper.pkindDefinition : Lean.ParserDescr

Equations

• Paper.pkindDefinition = Lean.ParserDescr.node `Paper.pkindDefinition 1024 (Lean.ParserDescr.symbol "Definition ")

def Paper.pkindTheorem : Lean.ParserDescr

Equations

• Paper.pkindTheorem = Lean.ParserDescr.node `Paper.pkindTheorem 1024 (Lean.ParserDescr.symbol "Theorem ")

def Paper.pkindLemma : Lean.ParserDescr

Equations

• Paper.pkindLemma = Lean.ParserDescr.node `Paper.pkindLemma 1024 (Lean.ParserDescr.symbol "Lemma ")

def Paper.«pkind@_» : Lean.ParserDescr

Equations

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

def Paper.«term[pkind|_]» : Lean.ParserDescr

Equations

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

def Paper.«command_Section_,__:_» : Lean.ParserDescr

Equations

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