Documentation
Iris
.
ProofMode
.
Tactics
.
Exact
Search
return to top
source
Imports
Init
Iris.ProofMode.Tactics.Basic
Iris.ProofMode.Tactics.Remove
Imported by
Iris
.
ProofMode
.
tacticIexact__
source
def
Iris
.
ProofMode
.
tacticIexact__
:
Lean.ParserDescr
Equations
One or more equations did not get rendered due to their size.
Instances For