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

doc: update RELEASES.md for #3495 (#3518)

Browse source
This commit is contained in:
Kyle Miller 2024-02-29 03:34:00 -08:00 • committed by GitHub
parent dc0f771561
commit 67c9498892
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
RELEASES.md
View file

@ -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