Def Mathlib.Meta.NormNum.deriveSimp

Modification history

2026-09-09 00:40
Mathlib/Tactic/NormNum/Core.lean
feat(Tactic/NormNum): run simp's default simprocs inside norm_num (#43003) …
Modified Mathlib.Meta.NormNum.deriveSimpView on Github →
2026-03-29 15:39
Mathlib/Tactic/NormNum/Core.lean
fix(Tactic/NormNum): do not re-enter `simp` from the very outside (#36841) …
Added Mathlib.Meta.NormNum.deriveSimpView on Github →