From a4dd9fe0598328976862868097f59207846d865c Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jun 2024 17:51:36 +0200 Subject: Regenerate the Coq and Lean betrees --- tests/lean/Betree/Funs.lean | 291 ++++++++++++++++++++++++++++++-------------- 1 file changed, 202 insertions(+), 89 deletions(-) (limited to 'tests/lean/Betree/Funs.lean') diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean index 8612ccbc..7d8b4714 100644 --- a/tests/lean/Betree/Funs.lean +++ b/tests/lean/Betree/Funs.lean @@ -79,42 +79,74 @@ def betree.upsert_update then prev1 - v else Result.ok 0#u64 +/- [betree::betree::{betree::betree::List#1}::len]: loop 0: + Source: 'src/betree.rs', lines 276:4-284:5 -/ +divergent def betree.List.len_loop + (T : Type) (self : betree.List T) (len : U64) : Result U64 := + match self with + | betree.List.Cons _ tl => + do + let len1 ← len + 1#u64 + betree.List.len_loop T tl len1 + | betree.List.Nil => Result.ok len + /- [betree::betree::{betree::betree::List#1}::len]: Source: 'src/betree.rs', lines 276:4-276:24 -/ -divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 := +def betree.List.len (T : Type) (self : betree.List T) : Result U64 := + betree.List.len_loop T self 0#u64 + +/- [betree::betree::{betree::betree::List#1}::reverse]: loop 0: + Source: 'src/betree.rs', lines 304:4-312:5 -/ +divergent def betree.List.reverse_loop + (T : Type) (self : betree.List T) (out : betree.List T) : + Result (betree.List T) + := match self with - | betree.List.Cons _ tl => do - let i ← betree.List.len T tl - 1#u64 + i - | betree.List.Nil => Result.ok 0#u64 - -/- [betree::betree::{betree::betree::List#1}::split_at]: - Source: 'src/betree.rs', lines 284:4-284:51 -/ -divergent def betree.List.split_at - (T : Type) (self : betree.List T) (n : U64) : + | betree.List.Cons hd tl => + betree.List.reverse_loop T tl (betree.List.Cons hd out) + | betree.List.Nil => Result.ok out + +/- [betree::betree::{betree::betree::List#1}::reverse]: + Source: 'src/betree.rs', lines 304:4-304:32 -/ +def betree.List.reverse + (T : Type) (self : betree.List T) : Result (betree.List T) := + betree.List.reverse_loop T self betree.List.Nil + +/- [betree::betree::{betree::betree::List#1}::split_at]: loop 0: + Source: 'src/betree.rs', lines 287:4-302:5 -/ +divergent def betree.List.split_at_loop + (T : Type) (n : U64) (beg : betree.List T) (self : betree.List T) : Result ((betree.List T) × (betree.List T)) := - if n = 0#u64 - then Result.ok (betree.List.Nil, self) - else + if n > 0#u64 + then match self with | betree.List.Cons hd tl => do - let i ← n - 1#u64 - let p ← betree.List.split_at T tl i - let (ls0, ls1) := p - Result.ok (betree.List.Cons hd ls0, ls1) + let n1 ← n - 1#u64 + betree.List.split_at_loop T n1 (betree.List.Cons hd beg) tl | betree.List.Nil => Result.fail .panic + else do + let l ← betree.List.reverse T beg + Result.ok (l, self) + +/- [betree::betree::{betree::betree::List#1}::split_at]: + Source: 'src/betree.rs', lines 287:4-287:55 -/ +def betree.List.split_at + (T : Type) (self : betree.List T) (n : U64) : + Result ((betree.List T) × (betree.List T)) + := + betree.List.split_at_loop T n betree.List.Nil self /- [betree::betree::{betree::betree::List#1}::push_front]: - Source: 'src/betree.rs', lines 299:4-299:34 -/ + Source: 'src/betree.rs', lines 315:4-315:34 -/ def betree.List.push_front (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) := let (tl, _) := core.mem.replace (betree.List T) self betree.List.Nil Result.ok (betree.List.Cons x tl) /- [betree::betree::{betree::betree::List#1}::pop_front]: - Source: 'src/betree.rs', lines 306:4-306:32 -/ + Source: 'src/betree.rs', lines 322:4-322:32 -/ def betree.List.pop_front (T : Type) (self : betree.List T) : Result (T × (betree.List T)) := let (ls, _) := core.mem.replace (betree.List T) self betree.List.Nil @@ -123,14 +155,14 @@ def betree.List.pop_front | betree.List.Nil => Result.fail .panic /- [betree::betree::{betree::betree::List#1}::hd]: - Source: 'src/betree.rs', lines 318:4-318:22 -/ + Source: 'src/betree.rs', lines 334:4-334:22 -/ def betree.List.hd (T : Type) (self : betree.List T) : Result T := match self with | betree.List.Cons hd _ => Result.ok hd | betree.List.Nil => Result.fail .panic /- [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]: - Source: 'src/betree.rs', lines 327:4-327:44 -/ + Source: 'src/betree.rs', lines 343:4-343:44 -/ def betree.ListPairU64T.head_has_key (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool := match self with @@ -138,26 +170,40 @@ def betree.ListPairU64T.head_has_key Result.ok (i = key) | betree.List.Nil => Result.ok false -/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: - Source: 'src/betree.rs', lines 339:4-339:73 -/ -divergent def betree.ListPairU64T.partition_at_pivot - (T : Type) (self : betree.List (U64 × T)) (pivot : U64) : +/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: loop 0: + Source: 'src/betree.rs', lines 355:4-370:5 -/ +divergent def betree.ListPairU64T.partition_at_pivot_loop + (T : Type) (pivot : U64) (beg : betree.List (U64 × T)) + (end1 : betree.List (U64 × T)) (self : betree.List (U64 × T)) : Result ((betree.List (U64 × T)) × (betree.List (U64 × T))) := match self with | betree.List.Cons hd tl => let (i, t) := hd if i >= pivot - then Result.ok (betree.List.Nil, betree.List.Cons (i, t) tl) + then + betree.ListPairU64T.partition_at_pivot_loop T pivot beg (betree.List.Cons + (i, t) end1) tl else - do - let p ← betree.ListPairU64T.partition_at_pivot T tl pivot - let (ls0, ls1) := p - Result.ok (betree.List.Cons (i, t) ls0, ls1) - | betree.List.Nil => Result.ok (betree.List.Nil, betree.List.Nil) + betree.ListPairU64T.partition_at_pivot_loop T pivot (betree.List.Cons (i, + t) beg) end1 tl + | betree.List.Nil => + do + let l ← betree.List.reverse (U64 × T) beg + let l1 ← betree.List.reverse (U64 × T) end1 + Result.ok (l, l1) + +/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: + Source: 'src/betree.rs', lines 355:4-355:73 -/ +def betree.ListPairU64T.partition_at_pivot + (T : Type) (self : betree.List (U64 × T)) (pivot : U64) : + Result ((betree.List (U64 × T)) × (betree.List (U64 × T))) + := + betree.ListPairU64T.partition_at_pivot_loop T pivot betree.List.Nil + betree.List.Nil self /- [betree::betree::{betree::betree::Leaf#3}::split]: - Source: 'src/betree.rs', lines 359:4-364:17 -/ + Source: 'src/betree.rs', lines 378:4-383:17 -/ def betree.Leaf.split (self : betree.Leaf) (content : betree.List (U64 × U64)) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) : @@ -176,9 +222,9 @@ def betree.Leaf.split let n1 := betree.Node.Leaf { id := id1, size := params.split_size } Result.ok (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2)) -/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: - Source: 'src/betree.rs', lines 789:4-792:34 -/ -divergent def betree.Node.lookup_first_message_for_key +/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: loop 0: + Source: 'src/betree.rs', lines 792:4-810:5 -/ +divergent def betree.Node.lookup_first_message_for_key_loop (key : U64) (msgs : betree.List (U64 × betree.Message)) : Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 × betree.Message) → Result (betree.List (U64 × betree.Message)))) @@ -190,19 +236,28 @@ divergent def betree.Node.lookup_first_message_for_key then Result.ok (betree.List.Cons (i, m) next_msgs, Result.ok) else do - let (l, lookup_first_message_for_key_back) ← - betree.Node.lookup_first_message_for_key key next_msgs - let back := + let (l, back) ← + betree.Node.lookup_first_message_for_key_loop key next_msgs + let back1 := fun ret => do - let next_msgs1 ← lookup_first_message_for_key_back ret + let next_msgs1 ← back ret Result.ok (betree.List.Cons (i, m) next_msgs1) - Result.ok (l, back) + Result.ok (l, back1) | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok) -/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: - Source: 'src/betree.rs', lines 636:4-636:80 -/ -divergent def betree.Node.lookup_in_bindings +/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: + Source: 'src/betree.rs', lines 792:4-795:34 -/ +def betree.Node.lookup_first_message_for_key + (key : U64) (msgs : betree.List (U64 × betree.Message)) : + Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 × + betree.Message) → Result (betree.List (U64 × betree.Message)))) + := + betree.Node.lookup_first_message_for_key_loop key msgs + +/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0: + Source: 'src/betree.rs', lines 649:4-660:5 -/ +divergent def betree.Node.lookup_in_bindings_loop (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) := match bindings with | betree.List.Cons hd tl => @@ -212,12 +267,18 @@ divergent def betree.Node.lookup_in_bindings else if i > key then Result.ok none - else betree.Node.lookup_in_bindings key tl + else betree.Node.lookup_in_bindings_loop key tl | betree.List.Nil => Result.ok none -/- [betree::betree::{betree::betree::Node#5}::apply_upserts]: - Source: 'src/betree.rs', lines 819:4-819:90 -/ -divergent def betree.Node.apply_upserts +/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: + Source: 'src/betree.rs', lines 649:4-649:84 -/ +def betree.Node.lookup_in_bindings + (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) := + betree.Node.lookup_in_bindings_loop key bindings + +/- [betree::betree::{betree::betree::Node#5}::apply_upserts]: loop 0: + Source: 'src/betree.rs', lines 820:4-844:5 -/ +divergent def betree.Node.apply_upserts_loop (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64) : Result (U64 × (betree.List (U64 × betree.Message))) @@ -235,7 +296,7 @@ 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 + betree.Node.apply_upserts_loop msgs1 (some v) key else do let v ← core.option.Option.unwrap U64 prev @@ -244,8 +305,17 @@ divergent def betree.Node.apply_upserts betree.Message.Insert v) Result.ok (v, msgs1) +/- [betree::betree::{betree::betree::Node#5}::apply_upserts]: + Source: 'src/betree.rs', lines 820:4-820:94 -/ +def betree.Node.apply_upserts + (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64) + : + Result (U64 × (betree.List (U64 × betree.Message))) + := + betree.Node.apply_upserts_loop msgs prev key + /- [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: - Source: 'src/betree.rs', lines 395:4-395:63 -/ + Source: 'src/betree.rs', lines 414:4-414:63 -/ mutual divergent def betree.Internal.lookup_in_children (self : betree.Internal) (key : U64) (st : State) : Result (State × ((Option U64) × betree.Internal)) @@ -261,7 +331,7 @@ mutual divergent def betree.Internal.lookup_in_children Result.ok (st1, (o, betree.Internal.mk self.id self.pivot self.left n)) /- [betree::betree::{betree::betree::Node#5}::lookup]: - Source: 'src/betree.rs', lines 709:4-709:58 -/ + Source: 'src/betree.rs', lines 712:4-712:58 -/ divergent def betree.Node.lookup (self : betree.Node) (key : U64) (st : State) : Result (State × ((Option U64) × betree.Node)) @@ -320,9 +390,9 @@ divergent def betree.Node.lookup end -/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: - Source: 'src/betree.rs', lines 674:4-674:77 -/ -divergent def betree.Node.filter_messages_for_key +/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: loop 0: + Source: 'src/betree.rs', lines 683:4-692:5 -/ +divergent def betree.Node.filter_messages_for_key_loop (key : U64) (msgs : betree.List (U64 × betree.Message)) : Result (betree.List (U64 × betree.Message)) := @@ -335,13 +405,21 @@ divergent def betree.Node.filter_messages_for_key let (_, msgs1) ← betree.List.pop_front (U64 × betree.Message) (betree.List.Cons (k, m) l) - betree.Node.filter_messages_for_key key msgs1 + betree.Node.filter_messages_for_key_loop key msgs1 else Result.ok (betree.List.Cons (k, m) l) | betree.List.Nil => Result.ok betree.List.Nil -/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: - Source: 'src/betree.rs', lines 689:4-692:34 -/ -divergent def betree.Node.lookup_first_message_after_key +/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: + Source: 'src/betree.rs', lines 683:4-683:77 -/ +def betree.Node.filter_messages_for_key + (key : U64) (msgs : betree.List (U64 × betree.Message)) : + Result (betree.List (U64 × betree.Message)) + := + betree.Node.filter_messages_for_key_loop key msgs + +/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: loop 0: + Source: 'src/betree.rs', lines 694:4-706:5 -/ +divergent def betree.Node.lookup_first_message_after_key_loop (key : U64) (msgs : betree.List (U64 × betree.Message)) : Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 × betree.Message) → Result (betree.List (U64 × betree.Message)))) @@ -352,19 +430,28 @@ divergent def betree.Node.lookup_first_message_after_key if k = key then do - let (l, lookup_first_message_after_key_back) ← - betree.Node.lookup_first_message_after_key key next_msgs - let back := + let (l, back) ← + betree.Node.lookup_first_message_after_key_loop key next_msgs + let back1 := fun ret => do - let next_msgs1 ← lookup_first_message_after_key_back ret + let next_msgs1 ← back ret Result.ok (betree.List.Cons (k, m) next_msgs1) - Result.ok (l, back) + Result.ok (l, back1) else Result.ok (betree.List.Cons (k, m) next_msgs, Result.ok) | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok) +/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: + Source: 'src/betree.rs', lines 694:4-697:34 -/ +def betree.Node.lookup_first_message_after_key + (key : U64) (msgs : betree.List (U64 × betree.Message)) : + Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 × + betree.Message) → Result (betree.List (U64 × betree.Message)))) + := + betree.Node.lookup_first_message_after_key_loop key msgs + /- [betree::betree::{betree::betree::Node#5}::apply_to_internal]: - Source: 'src/betree.rs', lines 521:4-521:89 -/ + Source: 'src/betree.rs', lines 534:4-534:89 -/ def betree.Node.apply_to_internal (msgs : betree.List (U64 × betree.Message)) (key : U64) (new_msg : betree.Message) : @@ -427,9 +514,9 @@ def betree.Node.apply_to_internal betree.List.push_front (U64 × betree.Message) msgs1 (key, new_msg) lookup_first_message_for_key_back msgs2 -/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: - Source: 'src/betree.rs', lines 502:4-505:5 -/ -divergent def betree.Node.apply_messages_to_internal +/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: loop 0: + Source: 'src/betree.rs', lines 518:4-526:5 -/ +divergent def betree.Node.apply_messages_to_internal_loop (msgs : betree.List (U64 × betree.Message)) (new_msgs : betree.List (U64 × betree.Message)) : Result (betree.List (U64 × betree.Message)) @@ -439,12 +526,21 @@ divergent def betree.Node.apply_messages_to_internal do let (i, m) := new_msg let msgs1 ← betree.Node.apply_to_internal msgs i m - betree.Node.apply_messages_to_internal msgs1 new_msgs_tl + betree.Node.apply_messages_to_internal_loop msgs1 new_msgs_tl | betree.List.Nil => Result.ok msgs -/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: - Source: 'src/betree.rs', lines 653:4-656:32 -/ -divergent def betree.Node.lookup_mut_in_bindings +/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: + Source: 'src/betree.rs', lines 518:4-521:5 -/ +def betree.Node.apply_messages_to_internal + (msgs : betree.List (U64 × betree.Message)) + (new_msgs : betree.List (U64 × betree.Message)) : + Result (betree.List (U64 × betree.Message)) + := + betree.Node.apply_messages_to_internal_loop msgs new_msgs + +/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: loop 0: + Source: 'src/betree.rs', lines 664:4-677:5 -/ +divergent def betree.Node.lookup_mut_in_bindings_loop (key : U64) (bindings : betree.List (U64 × U64)) : Result ((betree.List (U64 × U64)) × (betree.List (U64 × U64) → Result (betree.List (U64 × U64)))) @@ -456,18 +552,26 @@ divergent def betree.Node.lookup_mut_in_bindings then Result.ok (betree.List.Cons (i, i1) tl, Result.ok) else do - let (l, lookup_mut_in_bindings_back) ← - betree.Node.lookup_mut_in_bindings key tl - let back := + let (l, back) ← betree.Node.lookup_mut_in_bindings_loop key tl + let back1 := fun ret => do - let tl1 ← lookup_mut_in_bindings_back ret + let tl1 ← back ret Result.ok (betree.List.Cons (i, i1) tl1) - Result.ok (l, back) + Result.ok (l, back1) | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok) +/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: + Source: 'src/betree.rs', lines 664:4-667:32 -/ +def betree.Node.lookup_mut_in_bindings + (key : U64) (bindings : betree.List (U64 × U64)) : + Result ((betree.List (U64 × U64)) × (betree.List (U64 × U64) → Result + (betree.List (U64 × U64)))) + := + betree.Node.lookup_mut_in_bindings_loop key bindings + /- [betree::betree::{betree::betree::Node#5}::apply_to_leaf]: - Source: 'src/betree.rs', lines 460:4-460:87 -/ + Source: 'src/betree.rs', lines 476:4-476:87 -/ def betree.Node.apply_to_leaf (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message) : @@ -506,9 +610,9 @@ def betree.Node.apply_to_leaf let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v) lookup_mut_in_bindings_back bindings2 -/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: - Source: 'src/betree.rs', lines 444:4-447:5 -/ -divergent def betree.Node.apply_messages_to_leaf +/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: loop 0: + Source: 'src/betree.rs', lines 463:4-471:5 -/ +divergent def betree.Node.apply_messages_to_leaf_loop (bindings : betree.List (U64 × U64)) (new_msgs : betree.List (U64 × betree.Message)) : Result (betree.List (U64 × U64)) @@ -518,11 +622,20 @@ divergent def betree.Node.apply_messages_to_leaf do let (i, m) := new_msg let bindings1 ← betree.Node.apply_to_leaf bindings i m - betree.Node.apply_messages_to_leaf bindings1 new_msgs_tl + betree.Node.apply_messages_to_leaf_loop bindings1 new_msgs_tl | betree.List.Nil => Result.ok bindings +/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: + Source: 'src/betree.rs', lines 463:4-466:5 -/ +def betree.Node.apply_messages_to_leaf + (bindings : betree.List (U64 × U64)) + (new_msgs : betree.List (U64 × betree.Message)) : + Result (betree.List (U64 × U64)) + := + betree.Node.apply_messages_to_leaf_loop bindings new_msgs + /- [betree::betree::{betree::betree::Internal#4}::flush]: - Source: 'src/betree.rs', lines 410:4-415:26 -/ + Source: 'src/betree.rs', lines 429:4-434:26 -/ mutual divergent def betree.Internal.flush (self : betree.Internal) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) @@ -563,7 +676,7 @@ mutual divergent def betree.Internal.flush self.left n, node_id_cnt1))) /- [betree::betree::{betree::betree::Node#5}::apply_messages]: - Source: 'src/betree.rs', lines 588:4-593:5 -/ + Source: 'src/betree.rs', lines 601:4-606:5 -/ divergent def betree.Node.apply_messages (self : betree.Node) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) @@ -610,7 +723,7 @@ divergent def betree.Node.apply_messages end /- [betree::betree::{betree::betree::Node#5}::apply]: - Source: 'src/betree.rs', lines 576:4-582:5 -/ + Source: 'src/betree.rs', lines 589:4-595:5 -/ def betree.Node.apply (self : betree.Node) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message) @@ -625,7 +738,7 @@ def betree.Node.apply Result.ok (st1, (self1, node_id_cnt1)) /- [betree::betree::{betree::betree::BeTree#6}::new]: - Source: 'src/betree.rs', lines 849:4-849:60 -/ + Source: 'src/betree.rs', lines 848:4-848:60 -/ def betree.BeTree.new (min_flush_size : U64) (split_size : U64) (st : State) : Result (State × betree.BeTree) @@ -642,7 +755,7 @@ def betree.BeTree.new }) /- [betree::betree::{betree::betree::BeTree#6}::apply]: - Source: 'src/betree.rs', lines 868:4-868:47 -/ + Source: 'src/betree.rs', lines 867:4-867:47 -/ def betree.BeTree.apply (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) : Result (State × betree.BeTree) @@ -654,7 +767,7 @@ def betree.BeTree.apply Result.ok (st1, { self with node_id_cnt := nic, root := n }) /- [betree::betree::{betree::betree::BeTree#6}::insert]: - Source: 'src/betree.rs', lines 874:4-874:52 -/ + Source: 'src/betree.rs', lines 873:4-873:52 -/ def betree.BeTree.insert (self : betree.BeTree) (key : U64) (value : U64) (st : State) : Result (State × betree.BeTree) @@ -662,7 +775,7 @@ def betree.BeTree.insert betree.BeTree.apply self key (betree.Message.Insert value) st /- [betree::betree::{betree::betree::BeTree#6}::delete]: - Source: 'src/betree.rs', lines 880:4-880:38 -/ + Source: 'src/betree.rs', lines 879:4-879:38 -/ def betree.BeTree.delete (self : betree.BeTree) (key : U64) (st : State) : Result (State × betree.BeTree) @@ -670,7 +783,7 @@ def betree.BeTree.delete betree.BeTree.apply self key betree.Message.Delete st /- [betree::betree::{betree::betree::BeTree#6}::upsert]: - Source: 'src/betree.rs', lines 886:4-886:59 -/ + Source: 'src/betree.rs', lines 885:4-885:59 -/ def betree.BeTree.upsert (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State) : @@ -679,7 +792,7 @@ def betree.BeTree.upsert betree.BeTree.apply self key (betree.Message.Upsert upd) st /- [betree::betree::{betree::betree::BeTree#6}::lookup]: - Source: 'src/betree.rs', lines 895:4-895:62 -/ + Source: 'src/betree.rs', lines 894:4-894:62 -/ def betree.BeTree.lookup (self : betree.BeTree) (key : U64) (st : State) : Result (State × ((Option U64) × betree.BeTree)) -- cgit v1.2.3