lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

fix: remove special handling of numerals in `DiscrTree`

Open timotree3 opened this issue 11 months ago • 10 comments

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.)

timotree3 avatar Mar 14 '24 17:03 timotree3