max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: update RELEASES for rcases using the custom Nat eliminator (#3902)

Browse source 
Note for #3747.
This commit is contained in:
Kyle Miller 2024-04-13 10:56:06 -07:00 • committed by GitHub
parent c4bfe25d18
commit 40df539ef1
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
RELEASES.md
View file

@ -80,8 +80,10 @@ v4.8.0 (development in progress)
Gives custom eliminators for `Nat` so that `induction` and `cases` put goal states into terms of `0` and `n + 1`
rather than `Nat.zero` and `Nat.succ n`.
Added option `tactic.customEliminators` to control whether to use custom eliminators.
[#3629](https://github.com/leanprover/lean4/pull/3629) and
[#3655](https://github.com/leanprover/lean4/pull/3655).
Added a hack for `rcases`/`rintro`/`obtain` to use the custom eliminator for `Nat`.
[#3629](https://github.com/leanprover/lean4/pull/3629),
[#3655](https://github.com/leanprover/lean4/pull/3655), and
[#3747](https://github.com/leanprover/lean4/pull/3747).
* The `#guard_msgs` command now has options to change whitespace normalization and sensitivity to message ordering.
For example, `#guard_msgs (whitespace := lax) in cmd` collapses whitespace before checking messages,