Documentation
Lean
.
BuiltinDocAttr
Search
return to top
source
Imports
Lean.Compiler.InitAttr
Lean.DocString.Extension
Imported by
Lean
.
declareBuiltinDocStringAndRanges
source
def
Lean
.
declareBuiltinDocStringAndRanges
(declName :
Name
)
:
AttrM
Unit
Equations
One or more equations did not get rendered due to their size.
Instances For