Commit 2022-11-30 16:38 dc615a3b

View on Github →

feat: meta code for the category_theory port (#755)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Lean/Meta.lean

added def Lean.Meta.mapForallTelescope'

added def Lean.Meta.mapForallTelescope

Created Mathlib/Lean/Meta/Simp.lean

added def Lean.Meta.simpOnlyNames

added def Lean.Meta.simpTheoremsOfNames

added def Lean.Meta.simpType