Documentation
Lean
.
Elab
.
Tactic
.
Do
.
ProofMode
.
Have
Search
return to top
source
Imports
Std.Tactic.Do.Syntax
Lean.Elab.Tactic.Do.ProofMode.Cases
Lean.Elab.Tactic.Do.ProofMode.Specialize
Imported by
Lean
.
Elab
.
Tactic
.
Do
.
ProofMode
.
elabMDup
Lean
.
Elab
.
Tactic
.
Do
.
ProofMode
.
elabMHave
Lean
.
Elab
.
Tactic
.
Do
.
ProofMode
.
elabMReplace
source
def
Lean
.
Elab
.
Tactic
.
Do
.
ProofMode
.
elabMDup
:
Tactic
Equations
One or more equations did not get rendered due to their size.
Instances For
source
def
Lean
.
Elab
.
Tactic
.
Do
.
ProofMode
.
elabMHave
:
Tactic
Equations
One or more equations did not get rendered due to their size.
Instances For
source
def
Lean
.
Elab
.
Tactic
.
Do
.
ProofMode
.
elabMReplace
:
Tactic
Equations
One or more equations did not get rendered due to their size.
Instances For