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

chore: add error recovery to RELEASES.md (#3540)

Browse source 
Adds the missing RELEASES.md from #3413. Apologies for the oversight!
This commit is contained in:
David Thrane Christiansen 2024-03-01 06:38:18 +01:00 • committed by GitHub
parent ed02262941
commit 43d6eb144e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
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

@ -91,6 +91,8 @@ 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)
Breaking changes:
* `Lean.withTraceNode` and variants got a stronger `MonadAlwaysExcept` assumption to
fix trace trees not being built on elaboration runtime exceptions. Instances for most elaboration