Documentation
Batteries
.
Tactic
.
Lint
.
Simp
Search
return to top
source
Imports
Init
Batteries.Tactic.OpenPrivate
Batteries.Util.LibraryNote
Batteries.Tactic.Lint.Basic
Lean.Meta.Tactic.Simp.Main
Lean.Meta.Tactic.Simp.SimpTheorems
Imported by