Documentation
DY
.
Meta
.
Cleanup
Search
return to top
source
Imports
Init
Lean
Imported by
tacticCleanup
source
def
tacticCleanup
:
Lean.ParserDescr
Equations
tacticCleanup
=
Lean.ParserDescr.node
`tacticCleanup
1024
(
Lean.ParserDescr.nonReservedSymbol
"cleanup"
false
)
Instances For