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
    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
        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
            Instances For