Documentation
Lean
.
Elab
.
Tactic
.
Do
.
ProofMode
Search
return to top
source
Imports
Lean.Elab.Tactic.Do.ProofMode.Assumption
Lean.Elab.Tactic.Do.ProofMode.Basic
Lean.Elab.Tactic.Do.ProofMode.Cases
Lean.Elab.Tactic.Do.ProofMode.Clear
Lean.Elab.Tactic.Do.ProofMode.Constructor
Lean.Elab.Tactic.Do.ProofMode.Delab
Lean.Elab.Tactic.Do.ProofMode.Exact
Lean.Elab.Tactic.Do.ProofMode.Exfalso
Lean.Elab.Tactic.Do.ProofMode.Frame
Lean.Elab.Tactic.Do.ProofMode.Have
Lean.Elab.Tactic.Do.ProofMode.Intro
Lean.Elab.Tactic.Do.ProofMode.LeftRight
Lean.Elab.Tactic.Do.ProofMode.MGoal
Lean.Elab.Tactic.Do.ProofMode.Pure
Lean.Elab.Tactic.Do.ProofMode.Refine
Lean.Elab.Tactic.Do.ProofMode.RenameI
Lean.Elab.Tactic.Do.ProofMode.Revert
Lean.Elab.Tactic.Do.ProofMode.Specialize
Imported by
← Copula mathematical handbook