Commit 2023-03-16 23:07 df866c92

View on Github →

feat: merge Util.Simp and Lean.Meta.Simp, add 4 decls (#2397)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Lean/Meta/Simp.lean

added def Lean.Meta.DiscrTree.getElements

added def Lean.Meta.Simp.SimpTheorems.contains

added def Lean.Meta.Simp.addSimpAttr

added def Lean.Meta.Simp.addSimpAttrFromSyntax

added def Lean.Meta.Simp.addSimpTheorem'

added def Lean.Meta.Simp.getAllSimpAttrs

added def Lean.Meta.Simp.getAllSimpDecls

added def Lean.Meta.Simp.getPropHyps

added def Lean.Meta.Simp.isInSimpSet

added def Lean.Meta.Simp.mkCast

added def Lean.Meta.Simp.mkEqSymm

added def Lean.Meta.Simp.mkSimpContext'

added def Lean.Meta.Simp.mkSimpTheoremsFromConst'

added def Lean.Meta.Simp.simpOnlyNames

added def Lean.Meta.Simp.simpTheoremsOfNames

added def Lean.Meta.Simp.simpType

deleted def Lean.Meta.simpOnlyNames

deleted def Lean.Meta.simpTheoremsOfNames

deleted def Lean.Meta.simpType

added def Lean.PHashSet.toList

Modified Mathlib/Tactic/NormCast/Tactic.lean

Modified Mathlib/Tactic/ToAdditive.lean

Deleted Mathlib/Util/Simp.lean

deleted def Lean.Meta.DiscrTree.getElements

deleted def Lean.Meta.Simp.addSimpAttr

deleted def Lean.Meta.Simp.addSimpAttrFromSyntax

deleted def Lean.Meta.Simp.addSimpTheorem'

deleted def Lean.Meta.Simp.getPropHyps

deleted def Lean.Meta.Simp.mkCast

deleted def Lean.Meta.Simp.mkEqSymm

deleted def Lean.Meta.Simp.mkSimpContext'

deleted def Lean.Meta.Simp.mkSimpTheoremsFromConst'

deleted def Lean.PHashSet.toList