Documentation

Aesop.Frontend.Basic

source
def Lean.Parser.Category.Aesop.bool_lit :
Category
Instances For
    source
    def Aesop.Frontend.Parser.Aesop.bool_lit.quot :
    Lean.ParserDescr
    Instances For
      source
      def Aesop.Frontend.Parser.bool_litTrue :
      Lean.ParserDescr
      Instances For
        source
        def Aesop.Frontend.Parser.bool_litFalse :
        Lean.ParserDescr
        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
          Instances For