diff options
| author | Guillaume Boisseau | 2024-04-30 15:43:32 +0200 |
|---|---|---|
| committer | GitHub | 2024-04-30 15:43:32 +0200 |
| commit | 37cf570462cff897eaeb34d3a48179ae9597ce65 (patch) | |
| tree | 9e579a360d38b1a2f31cacc7429403fb39d691f0 /tests | |
| parent | fead40d1fb6e9f7bed705e8d3048133cf59c3bb8 (diff) | |
| parent | 5209b9976107592802327bac30e8b98fbb9c2d2f (diff) | |
Merge pull request #165 from AeneasVerif/bump-charon
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/coq/betree/BetreeMain_Funs.v | 2 | ||||
| -rw-r--r-- | tests/fstar/betree/BetreeMain.Funs.fst | 2 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 2 | ||||
| -rw-r--r-- | tests/lean/Betree.lean | 1 | ||||
| -rw-r--r-- | tests/lean/BetreeMain/Funs.lean | 2 |
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 () |