diff options
| author | Son Ho | 2024-04-25 16:28:30 +0200 |
|---|---|---|
| committer | Son Ho | 2024-04-25 16:28:30 +0200 |
| commit | 036756d6bddbcf9bc936489779ed36c7e4d22d14 (patch) | |
| tree | 01ab1e2e5d1bbbbceedb6683d0826f05bd0a5720 /tests/lean | |
| parent | eb5b2e76de6e2c6780b9817c1424777276ea5e00 (diff) | |
Regenerate and fix the tests
Diffstat (limited to 'tests/lean')
| -rw-r--r-- | tests/lean/BetreeMain/Funs.lean | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean index 0c31b9bc..f0032d51 100644 --- a/tests/lean/BetreeMain/Funs.lean +++ b/tests/lean/BetreeMain/Funs.lean @@ -219,8 +219,8 @@ divergent def betree.Node.lookup_in_bindings Source: 'src/betree.rs', lines 819:4-819:90 -/ divergent def betree.Node.apply_upserts (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64) - (st : State) : - Result (State × (U64 × (betree.List (U64 × betree.Message)))) + : + Result (U64 × (betree.List (U64 × betree.Message))) := do let b ← betree.ListPairU64T.head_has_key betree.Message msgs key @@ -235,14 +235,14 @@ divergent def betree.Node.apply_upserts | betree.Message.Upsert s => do let v ← betree.upsert_update prev s - betree.Node.apply_upserts msgs1 (some v) key st + betree.Node.apply_upserts msgs1 (some v) key 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 (v, msgs1) /- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 395:4-395:63 -/ @@ -307,13 +307,13 @@ divergent def betree.Node.lookup let (st2, (v, node1)) ← betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key st1 - let (st3, (v1, pending1)) ← + let (v1, pending1) ← betree.Node.apply_upserts (betree.List.Cons (k, - betree.Message.Upsert ufs) l) v key st2 + betree.Message.Upsert ufs) l) v key let ⟨ i2, i3, n2, n3 ⟩ := node1 let msgs1 ← lookup_first_message_for_key_back pending1 - let (st4, _) ← betree.store_internal_node i2 msgs1 st3 - Result.ok (st4, (some v1, betree.Node.Internal (betree.Internal.mk i2 + let (st3, _) ← betree.store_internal_node i2 msgs1 st2 + Result.ok (st3, (some v1, betree.Node.Internal (betree.Internal.mk i2 i3 n2 n3))) | betree.List.Nil => do |