From f3e16bb43a8ff27a5184d9fa452277cc6a59410f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 19 Mar 2024 05:29:29 +0100
Subject: Regenerate the tests

---
 tests/lean/BetreeMain/Funs.lean | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'tests/lean/BetreeMain')

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 -/
-- 
cgit v1.2.3