summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorGuillaume Boisseau2024-04-30 15:43:32 +0200
committerGitHub2024-04-30 15:43:32 +0200
commit37cf570462cff897eaeb34d3a48179ae9597ce65 (patch)
tree9e579a360d38b1a2f31cacc7429403fb39d691f0 /tests
parentfead40d1fb6e9f7bed705e8d3048133cf59c3bb8 (diff)
parent5209b9976107592802327bac30e8b98fbb9c2d2f (diff)
Merge pull request #165 from AeneasVerif/bump-charon
Diffstat (limited to 'tests')
-rw-r--r--tests/coq/betree/BetreeMain_Funs.v2
-rw-r--r--tests/fstar/betree/BetreeMain.Funs.fst2
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Funs.fst2
-rw-r--r--tests/lean/Betree.lean1
-rw-r--r--tests/lean/BetreeMain/Funs.lean2
5 files changed, 5 insertions, 4 deletions
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index c31713be..e0a1d8a2 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -827,7 +827,7 @@ Definition betree_BeTree_lookup
.
(** [betree_main::main]:
- Source: 'src/betree_main.rs', lines 5:0-5:9 *)
+ Source: 'src/main.rs', lines 4:0-4:9 *)
Definition main : result unit :=
Ok tt.
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index 89396df0..9942ef68 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -667,7 +667,7 @@ let betree_BeTree_lookup
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 *)
let main : result unit =
Ok ()
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 89396df0..9942ef68 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -667,7 +667,7 @@ let betree_BeTree_lookup
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 *)
let main : result unit =
Ok ()
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 ()