Documentation

Lean.BuiltinDocAttr

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