Documentation

Lean.DocString

def Lean.addBuiltinDocString (declName : Lake.Name) (docString : String) :
Instances For
    def Lean.addDocString {m : TypeType} [Lean.MonadEnv m] (declName : Lake.Name) (docString : String) :
    Instances For
      def Lean.addDocString' {m : TypeType} [Monad m] [Lean.MonadEnv m] (declName : Lake.Name) (docString? : Option String) :
      Instances For
        def Lean.findDocString? (env : Lean.Environment) (declName : Lake.Name) (includeBuiltin : optParam Bool true) :
        Instances For
          structure Lean.ModuleDoc :
          Instances For
            def Lean.getDocStringText {m : TypeType} [Monad m] [Lean.MonadError m] [Lean.MonadRef m] (stx : Lean.TSyntax `Lean.Parser.Command.docComment) :
            Instances For
              def Lean.TSyntax.getDocString (stx : Lean.TSyntax `Lean.Parser.Command.docComment) :
              Instances For