Documentation

Lean.DocString.Extension

def Lean.addBuiltinDocString (declName : Lake.Name) (docString : String) :
Equations
Instances For
    def Lean.addDocString {m : TypeType} [Monad m] [Lean.MonadError m] [Lean.MonadEnv m] (declName : Lake.Name) (docString : String) :
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def Lean.addDocString' {m : TypeType} [Monad m] [Lean.MonadError m] [Lean.MonadEnv m] (declName : Lake.Name) (docString? : Option String) :
      Equations
      Instances For
        def Lean.findSimpleDocString? (env : Lean.Environment) (declName : Lake.Name) (includeBuiltin : optParam Bool true) :

        Finds a docstring without performing any alias resolution or enrichment with extra metadata.

        Docstrings to be shown to a user should be looked up with Lean.findDocString? instead.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          structure Lean.ModuleDoc :
          Instances For
            Equations
            Instances For
              def Lean.getDocStringText {m : TypeType} [Monad m] [Lean.MonadError m] (stx : Lean.TSyntax `Lean.Parser.Command.docComment) :
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For