Zulip Chat Archive
Stream: mathlib4
Topic: PR to use lake
Scott Morrison (Oct 18 2021 at 00:14):
I have a PR for mathlib4 to use lake, now that it is bundled with the lean4 nightlies. Could someone please review? It will simplify the mathport process once everything is on lake.
Last updated: Feb 28 2026 at 14:05 UTC