Def Mathlib.Meta.NormNum.evalSub.core

Modification history

2025-08-20 15:48
Mathlib/Tactic/NormNum/Basic.lean
refactor(Tactic/NormNum): expose the derive API for known expressions directly (#28621) …
Deleted Mathlib.Meta.NormNum.evalSub.coreView on Github →
2025-08-19 08:36
Mathlib/Tactic/NormNum/Basic.lean
chore(Tactic/NormNum): make clear the current signature of the `core` functions (#28624) …
Added Mathlib.Meta.NormNum.evalSub.coreView on Github →