Def Mathlib.Meta.NormNum.NormNums.erase

Modification history

2024-07-15 16:11
Mathlib/Tactic/NormNum/Core.lean
chore(Tactic/NormNum): remove autoImplicit (#14725) …
Modified Mathlib.Meta.NormNum.NormNums.eraseView on Github →
2023-01-17 03:10
Mathlib/Tactic/NormNum/Core.lean
feat: make `norm_num` erasable (and scoped) (#1364) …
Added Mathlib.Meta.NormNum.NormNums.eraseView on Github →