Structure Mathlib.Meta.NormNum.NormNums

Modification history

2023-01-17 03:10
Mathlib/Tactic/NormNum/Core.lean
feat: make `norm_num` erasable (and scoped) (#1364) …
Added Mathlib.Meta.NormNum.NormNumsView on Github →