summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean')
-rw-r--r--tests/lean/Betree.lean1
-rw-r--r--tests/lean/BetreeMain/Funs.lean2
2 files changed, 2 insertions, 1 deletions
diff --git a/tests/lean/Betree.lean b/tests/lean/Betree.lean
new file mode 100644
index 00000000..58bee0c4
--- /dev/null
+++ b/tests/lean/Betree.lean
@@ -0,0 +1 @@
+import Betree.Funs
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index f0032d51..7cc52159 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -702,7 +702,7 @@ def betree.BeTree.lookup
Result.ok (st1, (o, { self with root := n }))
/- [betree_main::main]:
- Source: 'src/betree_main.rs', lines 5:0-5:9 -/
+ Source: 'src/main.rs', lines 4:0-4:9 -/
def main : Result Unit :=
Result.ok ()