summaryrefslogtreecommitdiff
path: root/tests/fstar/betree/BetreeMain.Clauses.Template.fst
diff options
context:
space:
mode:
authorSon Ho2023-12-05 15:00:46 +0100
committerSon Ho2023-12-05 15:00:46 +0100
commit60ce69b83cbd749781543bb16becb5357f0e1a0a (patch)
treebd847cb3ed7a00644ea643325468e5328f06e220 /tests/fstar/betree/BetreeMain.Clauses.Template.fst
parent054d7256ed90f752ae6b39ebba608f89076d38e7 (diff)
Update following changes in Charon
Diffstat (limited to 'tests/fstar/betree/BetreeMain.Clauses.Template.fst')
-rw-r--r--tests/fstar/betree/BetreeMain.Clauses.Template.fst14
1 files changed, 7 insertions, 7 deletions
diff --git a/tests/fstar/betree/BetreeMain.Clauses.Template.fst b/tests/fstar/betree/BetreeMain.Clauses.Template.fst
index 4ae29302..537705c5 100644
--- a/tests/fstar/betree/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree/BetreeMain.Clauses.Template.fst
@@ -33,6 +33,13 @@ let betree_Node_lookup_first_message_for_key_decreases (key : u64)
(msgs : betree_List_t (u64 & betree_Message_t)) : nat =
admit ()
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: decreases clause
+ Source: 'src/betree.rs', lines 636:4-636:80 *)
+unfold
+let betree_Node_lookup_in_bindings_decreases (key : u64)
+ (bindings : betree_List_t (u64 & u64)) : nat =
+ admit ()
+
(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: decreases clause
Source: 'src/betree.rs', lines 819:4-819:90 *)
unfold
@@ -41,13 +48,6 @@ let betree_Node_apply_upserts_decreases
(key : u64) (st : state) : nat =
admit ()
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: decreases clause
- Source: 'src/betree.rs', lines 636:4-636:80 *)
-unfold
-let betree_Node_lookup_in_bindings_decreases (key : u64)
- (bindings : betree_List_t (u64 & u64)) : nat =
- admit ()
-
(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause
Source: 'src/betree.rs', lines 395:4-395:63 *)
unfold