chore: use lakefile.toml

bergmannjg · Feb 5, 2025 · 3ccbaee · 3ccbaee
1 parent fc60c92
commit 3ccbaee
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 13 deletions.
diff --git a/lakefile.lean b/lakefile.lean
diff --git a/lakefile.toml b/lakefile.toml
@@ -0,0 +1,16 @@
+name = "time"
+lintDriver = "batteries/runLinter"
+defaultTargets = ["Time"]
+
+[[require]]
+name = "batteries"
+git = "https://github.com/leanprover-community/batteries"
+rev = "v4.16.0"
+
+[[require]]
+name = "tryAtEachStep"
+git = "https://github.com/dwrensha/tryAtEachStep"
+rev = "lean-v4.16.0"
+
+[[lean_lib]]
+name = "Time"