Documentation
Iris
.
Std
.
DelabRule
Search
return to top
source
Imports
Init
Lean.PrettyPrinter.Delaborator
Imported by
Iris
.
Std
.
commandDelab_rule__
source
def
Iris
.
Std
.
commandDelab_rule__
:
Lean.ParserDescr
Equations
One or more equations did not get rendered due to their size.
Instances For