aboutsummaryrefslogtreecommitdiff
path: root/LeanAStar.lean
diff options
context:
space:
mode:
authorAndreas Grois <andi@grois.info>2025-01-04 18:33:05 +0100
committerAndreas Grois <andi@grois.info>2025-01-04 18:33:05 +0100
commit3514e38cf48b611abc808b7de4c13862d3a4ede0 (patch)
tree9e4e3611259b8e8762bc92fd1a8fbd05a1012098 /LeanAStar.lean
Initial Commit (untested)
Diffstat (limited to 'LeanAStar.lean')
-rw-r--r--LeanAStar.lean4
1 files changed, 4 insertions, 0 deletions
diff --git a/LeanAStar.lean b/LeanAStar.lean
new file mode 100644
index 0000000..1008217
--- /dev/null
+++ b/LeanAStar.lean
@@ -0,0 +1,4 @@
+-- This module serves as the root of the `LeanAstar` library.
+-- Import modules here that should be built as part of the library.
+import LeanAStar.Basic
+import LeanAStar.Finite