From 40df539ef15406b66cc43baf99d738b940010700 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 13 Apr 2024 10:56:06 -0700 Subject: [PATCH] doc: update RELEASES for `rcases` using the custom `Nat` eliminator (#3902) Note for #3747. --- RELEASES.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/RELEASES.md b/RELEASES.md index af2bb20fee..2e03f7e51e 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -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,