summaryrefslogtreecommitdiff
path: root/tests/lean/BetreeMain
diff options
context:
space:
mode:
authorSon Ho2024-03-19 05:29:29 +0100
committerSon Ho2024-03-19 05:29:29 +0100
commitf3e16bb43a8ff27a5184d9fa452277cc6a59410f (patch)
treef79760b40b3a9f404b1db0d61f9d452408ef1de5 /tests/lean/BetreeMain
parent5a1373f5492f65ff0da6f7e0c34b056a98070908 (diff)
Regenerate the tests
Diffstat (limited to 'tests/lean/BetreeMain')
-rw-r--r--tests/lean/BetreeMain/Funs.lean8
1 files changed, 2 insertions, 6 deletions
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index d6449b37..bd5921a8 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -21,9 +21,7 @@ def betree.store_internal_node
(id : U64) (content : betree.List (U64 × betree.Message)) (st : State) :
Result (State × Unit)
:=
- do
- let (st1, _) ← betree_utils.store_internal_node id content st
- Result.ret (st1, ())
+ betree_utils.store_internal_node id content st
/- [betree_main::betree::load_leaf_node]:
Source: 'src/betree.rs', lines 46:0-46:44 -/
@@ -37,9 +35,7 @@ def betree.store_leaf_node
(id : U64) (content : betree.List (U64 × U64)) (st : State) :
Result (State × Unit)
:=
- do
- let (st1, _) ← betree_utils.store_leaf_node id content st
- Result.ret (st1, ())
+ betree_utils.store_leaf_node id content st
/- [betree_main::betree::fresh_node_id]:
Source: 'src/betree.rs', lines 55:0-55:48 -/