Documentation
Lean
.
Meta
.
Tactic
.
Simp
Search
return to top
source
Imports
Lean.Meta.Tactic.Simp.Arith
Lean.Meta.Tactic.Simp.Attr
Lean.Meta.Tactic.Simp.BuiltinSimprocs
Lean.Meta.Tactic.Simp.Diagnostics
Lean.Meta.Tactic.Simp.Main
Lean.Meta.Tactic.Simp.RegisterCommand
Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Tactic.Simp.Types
Imported by
Lean.Elab.Tactic.BVDecide.Frontend.Normalize.EmbeddedConstraint
Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Structures
Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Enums
Lean.Meta.Tactic
Lean.Elab.Tactic.BVDecide.Frontend.Normalize.ApplyControlFlow
Lean.Elab.Tactic.TreeTacAttr
Lean.Elab.Tactic.Simp