Commit 2025-01-01 21:42 9232fbe1

View on Github →

refactor: add an ofNat() elaborator (#20169) ofNat(n) is a shorthand for no_index (OfNat.ofNat n). Its purpose is:

  • To make it easier to remember to write the no_index
  • To add a place to put a hoverable docstrings explaining the complexities
  • To make it easier to remove the no_indexes in future if DiscrTrees stops needing them around ofNat (https://github.com/leanprover/lean4/issues/2867). This is not exhaustive, but is a step in the right direction. For now, I only target (some of) the declarations with a See note [no_index around OfNat.ofNat]. Some theorem statements have been corrected in passing. This exposed two Lean bugs relating to not using Expr.consumeMData:
  • leanprover/lean4#6438
  • leanprover/lean4#6467 These are made more likely by this PR adding no_index to the RHS of equalities, but were already possible to trigger by using simp [<- _] on existing theorems with no_index on the LHS.

Estimated changes

modified theorem CharP.ofNat_eq_zero
modified theorem DirectSum.of_zero_ofNat
modified theorem zpow_ofNat
modified theorem Int.ceil_ofNat
modified theorem Int.floor_ofNat
modified theorem Nat.ceil_ofNat
modified theorem Nat.floor_ofNat
modified theorem round_ofNat
modified theorem WithBot.bot_ne_ofNat
modified theorem WithBot.ofNat_ne_bot
modified theorem WithTop.ofNat_ne_top
modified theorem WithTop.top_ne_ofNat
modified theorem Int.sqrt_ofNat
modified theorem Nat.ofNat_pos'
modified theorem Rat.den_ofNat
modified theorem Rat.num_ofNat