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-04-13 10:32:36 -07:00
parent bcb9c2c2a3
commit f875c2d107
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
RELEASES.md
View file

@ -16,6 +16,8 @@ inductive LE' : Nat → Nat → Prop where
In both cases, the inductive family has one parameter and one index.
Recall that the actual number of parameters can be retrieved using the command `#print`.
* Remove support for `{}` annotation in the `structure` command.
* Several improvements to LSP server. Examples: "jump to definition" in mutually recursive sections, fixed incorrect hover information in "match"-expression patterns, "jump to definition" for pattern variables, fixed auto-completion in function headers, etc.
* In `macro ... xs:p* ...` and similar macro bindings of combinators, `xs` now has the correct type `Array Syntax`