Documentation

Aesop.Frontend.Basic

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