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

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

Instances For

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

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

Instances For

source
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)

Instances For

source
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)

Instances For

source
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.

Instances For