Commit 2023-11-20 00:38 d98fa2bf

View on Github →

chore: rewrite lakefile.lean (#8456) Reorganize lakefile.lean, and remove unnecessary stuff.

Estimated changes