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

chore: update release notes

Browse source
This commit is contained in:
Leonardo de Moura 2022-09-30 09:31:03 -07:00
parent 955a251bfc
commit c7fad1815c
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
RELEASES.md
View file

@ -1,6 +1,14 @@
Unreleased
---------
* [Hover information for `cases`/`induction` case names](https://github.com/leanprover/lean4/pull/1660).
* [Prefer longer parse even if unsuccessful](https://github.com/leanprover/lean4/pull/1658).
* [Show declaration module in hover](https://github.com/leanprover/lean4/pull/1638).
* [New `conv` mode structuring tactics](https://github.com/leanprover/lean4/pull/1636).
* `simp` can track information and can print an equivalent `simp only`. [PR #1626](https://github.com/leanprover/lean4/pull/1626).
* Enforce uniform indentation in tactic blocks / do blocks. See issue [#1606](https://github.com/leanprover/lean4/issues/1606).