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

chore: update Lake

Browse source
This commit is contained in:
tydeu 2022-08-05 23:30:46 -04:00 • committed by Sebastian Ullrich
parent 9a16d4afce
commit e470dad36c
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
RELEASES.md
View file

@ -1,6 +1,8 @@
Unreleased
---------
* Update Lake to v4.0.0. See the [v4.0.0 release notes](https://github.com/leanprover/lake/releases/tag/v4.0.0) for detailed changes.
* Mutual declarations in different namespaces are now supported. Example:
```lean
mutual
@ -251,8 +253,6 @@ Unreleased
end Nat
```
* Update Lake to v3.2.1. See the [v3.2.1 release notes](https://github.com/leanprover/lake/releases/tag/v3.2.1) for detailed changes.
* Add support for `CommandElabM` monad at `#eval`. Example:
```lean
import Lean

2
src/lake

@ -1 +1 @@
Subproject commit dcf8e1fc406acfd4dbbfd691f4ecf76966fae407
Subproject commit b899c0abac7d6c7ad69c06cd5b7964ac5684d3f0