← Copula mathematical handbook

def Lean.Parser.Category.Aesop.bool_lit : Category

Equations

• Lean.Parser.Category.Aesop.bool_lit = { }

def Aesop.Frontend.Parser.Aesop.bool_lit.quot : Lean.ParserDescr

Equations

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

def Aesop.Frontend.Parser.bool_litTrue : Lean.ParserDescr

Equations

• Aesop.Frontend.Parser.bool_litTrue = Lean.ParserDescr.node `Aesop.Frontend.Parser.bool_litTrue 1024 (Lean.ParserDescr.nonReservedSymbol "true" false)

def Aesop.Frontend.Parser.bool_litFalse : Lean.ParserDescr

Equations

• Aesop.Frontend.Parser.bool_litFalse = Lean.ParserDescr.node `Aesop.Frontend.Parser.bool_litFalse 1024 (Lean.ParserDescr.nonReservedSymbol "false" false)

def Aesop.Frontend.elabBoolLit {m : Type → Type} [Monad m] [Lean.MonadRef m] [MonadExceptOf Lean.Exception m] (stx : Lean.TSyntax `Aesop.bool_lit) : m Bool

Equations

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