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 2023-01-28 11:09:35 -05:00 • committed by Sebastian Ullrich
parent b69fcbc28f
commit 38a0d1e373
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,14 +1,14 @@
Unreleased
---------
* Update Lake to latest prerelease.
* [Make go-to-definition on a typeclass projection application go to the instance(s)](https://github.com/leanprover/lean4/pull/1767).
* [Include timings in trace messages when `profiler` is true](https://github.com/leanprover/lean4/pull/1995).
* [Pretty-print signatures in hover and `#check <ident>`](https://github.com/leanprover/lean4/pull/1943).
* [Update Lake to latest prerelease](https://github.com/leanprover/lean4/pull/1879).
* [Introduce parser memoization to avoid exponentional behavior](https://github.com/leanprover/lean4/pull/1799).
* [feat: allow `doSeq` in `let x <- e | seq`](https://github.com/leanprover/lean4/pull/1809).

2
src/lake

@ -1 +1 @@
Subproject commit d0b530530f14dde97a547b03abf87eee06360d60
Subproject commit db2c6a6707dcb58574884de512c2ab9bfc5ea3fc