From 67c9498892bfb3bd20e24ceca4c94b467e735ad4 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 29 Feb 2024 03:34:00 -0800 Subject: [PATCH] doc: update RELEASES.md for #3495 (#3518) --- RELEASES.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/RELEASES.md b/RELEASES.md index c68091edea..eb9ae5067b 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -18,6 +18,10 @@ v4.7.0 (development in progress) * `pp.proofs.withType` is now set to false by default to reduce noise in the info view. +* The pretty printer for applications now handles the case of over-application itself when applying app unexpanders. + In particular, the ``| `($_ $a $b $xs*) => `(($a + $b) $xs*)`` case of an `app_unexpander` is no longer necessary. + [#3495](https://github.com/leanprover/lean4/pull/3495). + * New `simp` (and `dsimp`) configuration option: `zetaDelta`. It is `false` by default. The `zeta` option is still `true` by default, but their meaning has changed. - When `zeta := true`, `simp` and `dsimp` reduce terms of the form