Documentation

Lean.Elab.DocString.Builtin.Parsing

source
def Lean.Doc.onlyCodes {m : Type → Type} [Monad m] [MonadError m] (xs : TSyntaxArray `Lean.Doc.Parser.inline) :
m (Array VersoCode)

Requires that all non-whitespace arguments to a role are code elements, returning their content if so. Throws an error otherwise.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Doc.onlyCode {m : Type → Type} [Monad m] [MonadError m] (xs : TSyntaxArray `Lean.Doc.Parser.inline) :
    m VersoCode

    Requires that the non-whitespace arguments to a role are a single code element, returning its content if so. Throws an error otherwise.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Doc.parseContent {m : Type → Type} [Monad m] [MonadFileMap m] [MonadEnv m] [MonadError m] [MonadLog m] [MonadOptions m] (p : Parser.ParserFn) (tok : Syntax) (contents : String) :
      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.parseContent' {m : Type → Type} [Monad m] [MonadFileMap m] [MonadEnv m] [AddMessageContext m] [MonadLog m] [MonadOptions m] (p : Parser.ParserFn) (tok : Syntax) (contents : String) :
          m (Syntax × Bool)
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lean.Doc.parseVersoCode {m : Type → Type} [Monad m] [MonadFileMap m] [MonadEnv m] [MonadError m] [MonadLog m] [MonadOptions m] (p : Parser.ParserFn) (c : VersoCode) :
            m Syntax

            Parses the contents of an inline code element.

            Equations
            Instances For
              source
              def Lean.Doc.parseVersoCodeBlock {m : Type → Type} [Monad m] [MonadFileMap m] [MonadEnv m] [MonadError m] [MonadLog m] [MonadOptions m] (p : Parser.ParserFn) (c : VersoCodeBlock) :
              m Syntax

              Parses the contents of a code block.

              Equations
              Instances For
                source
                def Lean.Doc.parseVersoCode' {m : Type → Type} [Monad m] [MonadFileMap m] [MonadEnv m] [AddMessageContext m] [MonadLog m] [MonadOptions m] (p : Parser.ParserFn) (c : VersoCode) :
                m (Syntax × Bool)

                Parses the contents of an inline code element, reporting errors rather than throwing.

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

                  Parses the contents of a string literal argument.

                  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)

                    Parses the contents of a string literal argument, reporting errors rather than throwing.

                    Equations
                    Instances For