Documentation
Lean
.
Meta
.
Sym
.
Simp
Search
return to top
source
Imports
Lean.Meta.Sym.Simp.App
Lean.Meta.Sym.Simp.Arith
Lean.Meta.Sym.Simp.Attr
Lean.Meta.Sym.Simp.CongrInfo
Lean.Meta.Sym.Simp.ControlFlow
Lean.Meta.Sym.Simp.Debug
Lean.Meta.Sym.Simp.Discharger
Lean.Meta.Sym.Simp.DiscrTree
Lean.Meta.Sym.Simp.EvalGround
Lean.Meta.Sym.Simp.Forall
Lean.Meta.Sym.Simp.Goal
Lean.Meta.Sym.Simp.Have
Lean.Meta.Sym.Simp.Lambda
Lean.Meta.Sym.Simp.Main
Lean.Meta.Sym.Simp.Reduce
Lean.Meta.Sym.Simp.RegisterCommand
Lean.Meta.Sym.Simp.Result
Lean.Meta.Sym.Simp.Rewrite
Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Simproc
Lean.Meta.Sym.Simp.Telescope
Lean.Meta.Sym.Simp.Theorems
Lean.Meta.Sym.Simp.Variant
Imported by