Documentation
Lean
.
Elab
.
Tactic
.
AsAuxLemma
Search
return to top
source
Imports
Lean.Elab.Tactic.Meta
Imported by
elabAsAuxLemma
source
def
elabAsAuxLemma
:
Lean.Elab.Tactic.Tactic
Equations
One or more equations did not get rendered due to their size.
Instances For