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

chore: add release notes for #3507 and #3509 (#3583)

Browse source
This commit is contained in:
Scott Morrison 2024-03-04 11:55:53 +11:00 • committed by GitHub
parent acb1b09fbf
commit ad901498fa
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
RELEASES.md
View file

@ -11,6 +11,12 @@ of each version.
v4.7.0 (development in progress)
---------
* `simp` and `rw` now use instance arguments found by unification,
rather than always resynthesizing. For backwards compatibility, the original behaviour is
available via `set_option tactic.skipAssignedInstances false`.
[#3507](https://github.com/leanprover/lean4/pull/3507) and
[#3509](https://github.com/leanprover/lean4/pull/3509).
* When the `pp.proofs` is false, now omitted proofs use `⋯` rather than `_`,
which gives a more helpful error message when copied from the Infoview.
The `pp.proofs.threshold` option lets small proofs always be pretty printed.
@ -94,7 +100,7 @@ v4.7.0 (development in progress)
* Changed call hierarchy to sort entries and strip private header from names displayed in the call hierarchy. [#3482](https://github.com/leanprover/lean4/pull/3482)
* There is now a low-level error recovery combinator in the parsing framework, primarily intended for DSLs. [#3413](https://github.com/leanprover/lean4/pull/3413)
* The Library search `exact?` and `apply?` tactics that were originally in
* The library search tactics `exact?` and `apply?` that were originally in
Mathlib are now available in Lean itself. These use the implementation using
lazy discrimination trees from `Std`, and thus do not require a disk cache but