From 1728dced8484befe35ef61fdf4ccd62b93fbb19d Mon Sep 17 00:00:00 2001
From: Zyad Hassan
Date: Wed, 24 Apr 2024 10:01:27 -0700
Subject: Fix a couple of tests

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

(limited to 'tests/lean/BetreeMain/Funs.lean')

diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 0c31b9bc..57b334fa 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -238,11 +238,11 @@ divergent def betree.Node.apply_upserts
       betree.Node.apply_upserts msgs1 (some v) key st
   else
     do
-    let (st1, v) ← core.option.Option.unwrap U64 prev st
+    let v ← core.option.Option.unwrap U64 prev
     let msgs1 ←
       betree.List.push_front (U64 × betree.Message) msgs (key,
         betree.Message.Insert v)
-    Result.ok (st1, (v, msgs1))
+    Result.ok (st, (v, msgs1))
 
 /- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]:
    Source: 'src/betree.rs', lines 395:4-395:63 -/
-- 
cgit v1.2.3