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

doc: add typed macros to RELEASES.md

Browse source
This commit is contained in:
Sebastian Ullrich 2022-06-27 23:42:13 +02:00
parent 5901fef43a
commit 18d2296b1c
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

@ -1,6 +1,8 @@
Unreleased
---------
* Add ["Typed Macros"](https://github.com/leanprover/lean4/pull/1251): syntax trees produced and accepted by syntax antiquotations now remember their syntax kinds, preventing accidental production of ill-formed syntax trees and reducing the need for explicit `:kind` antiquotation annotations. See PR for details.
* Aliases of protected definitions are protected too. Example:
```lean
protected def Nat.double (x : Nat) := 2*x