lean4
lean4 copied to clipboard
fix: remove special handling of numerals in `DiscrTree`
Fixes https://github.com/leanprover/lean4/issues/2867 by removing special handling of OfNat.ofNat
numerals from DiscrTree
.
The special handling was added in 2b8e55c2f19e6599128bc7e57cb7221df5693b4e to fix a bug represented in the test tests/lean/run/bugNatLitDiscrTree.lean
, but with https://github.com/leanprover/lean4/issues/2916 fixed, that test case passes without the special handling.
Some special handling of Nat.zero
and Nat.succ
remains to ensure that keys continue to match when unification replaces constants of the form Nat.zero...succ.succ
with numerals.
One notable implication of the removal of this special handling is that it means that instances of OfNat MyType n
for specific natural numbers n
should be written as OfNat MyType (nat_lit n)
. See tests/run/rewrites.lean for an example of this modification being needed.
Since this PR changes the persisted discrimination tree format, an update stage0
commit is necessary to make tests pass. (Otherwise oleans produced by the stage0 compiler with old discrimination tree data are used alongside the new discrimination tree algorithm.)