Merge pull request #48 from AeneasVerif/son_closures

Prepare support for function pointers and closures

1 files changed, 7 insertions, 7 deletions

diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst b/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
index 4ae29302..537705c5 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Clauses.Template.fst
+++ b/tests/fstar/betree_back_stateful/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