Documentation

Lean.BuiltinDocAttr

source
def Lean.declareBuiltinDocStringAndRanges (declName : Lean.Name) :
Lean.AttrM Unit
Instances For