Def Mathlib.Meta.NormNum.NormNums.eraseCore

Modification history

2023-01-17 03:10

Mathlib/Tactic/NormNum/Core.lean

feat: make `norm_num` erasable (and scoped) (#1364) …

Added Mathlib.Meta.NormNum.NormNums.eraseCore View on Github →