Documentation

Lean.Elab.DocString.Builtin.Parsing

source
def Lean.Doc.parseStrLit {m : Type → Type} [Monad m] [MonadFileMap m] [MonadEnv m] [MonadError m] [MonadLog m] [MonadOptions m] (p : Parser.ParserFn) (s : StrLit) :
m Syntax
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Doc.parseQuotedStrLit {m : Type → Type} [Monad m] [MonadFileMap m] [MonadEnv m] [MonadError m] [MonadLog m] [MonadOptions m] (p : Parser.ParserFn) (strLit : StrLit) :
    m Syntax
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Doc.parseStrLit' {m : Type → Type} [Monad m] [MonadFileMap m] [MonadEnv m] [AddMessageContext m] [MonadLog m] [MonadOptions m] (p : Parser.ParserFn) (s : StrLit) :
      m (Syntax × Bool)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For