Documentation
Std
.
Tactic
.
Basic
Search
Google site search
return to top
source
Imports
Init
Std.Linter
Std.Tactic.Init
Std.Tactic.SeqFocus
Std.Util.ProofWanted
Lean.Elab.Tactic.ElabTerm
Imported by