chore: replace lakefile.lean with a TOML version

I also enabled the `pp.proofs.withType` option.
chabulhwi · Dec 24, 2024 · c885f26 · c885f26
1 parent 22dcfcc
commit c885f26
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 14 deletions.
diff --git a/lakefile.lean b/lakefile.lean
diff --git a/lakefile.toml b/lakefile.toml
@@ -0,0 +1,8 @@
+name = "«tpil-solutions»"
+defaultTargets = ["TPIL"]
+
+[leanOptions]
+pp.unicode.fun = true
+
+[[lean_lib]]
+name = "TPIL"