TorchLean API

Docs HomeGuideExamplesGraphs

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