Documentation
Lean
.
Meta
.
Sym
.
Simp
Search
return to top
source
Imports
Lean.Meta.Sym.Simp.App
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.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
← Copula mathematical handbook