Documentation
Lean
.
Elab
.
Tactic
.
AsAuxLemma
Search
return to top
source
Imports
Init.Tactics
Lean.MetavarContext
Lean.Meta.Closure
Lean.Elab.Tactic.Basic
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