Documentation

Aesop.Frontend.Basic

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