From 6a467c040838e506316c8c72a701c2f61ff0ad1b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 6 May 2022 10:01:49 +0200
Subject: Generate F* files for the betree

---
 tests/betree/BetreeMain.Opaque.fsti | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)
 create mode 100644 tests/betree/BetreeMain.Opaque.fsti

(limited to 'tests/betree/BetreeMain.Opaque.fsti')

diff --git a/tests/betree/BetreeMain.Opaque.fsti b/tests/betree/BetreeMain.Opaque.fsti
new file mode 100644
index 00000000..7f0c04de
--- /dev/null
+++ b/tests/betree/BetreeMain.Opaque.fsti
@@ -0,0 +1,30 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [betree_main]: opaque function definitions *)
+module BetreeMain.Opaque
+open Primitives
+include BetreeMain.Types
+
+#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+
+(** [betree_main::betree_utils::load_internal_node] *)
+val betree_utils_load_internal_node_fwd
+  : u64 -> state -> result (state & (betree_list_t (u64 & betree_message_t)))
+
+(** [betree_main::betree_utils::store_internal_node] *)
+val betree_utils_store_internal_node_fwd
+  :
+  u64 -> betree_list_t (u64 & betree_message_t) -> state -> result (state &
+    unit)
+
+(** [betree_main::betree_utils::load_leaf_node] *)
+val betree_utils_load_leaf_node_fwd
+  : u64 -> state -> result (state & (betree_list_t (u64 & u64)))
+
+(** [betree_main::betree_utils::store_leaf_node] *)
+val betree_utils_store_leaf_node_fwd
+  : u64 -> betree_list_t (u64 & u64) -> state -> result (state & unit)
+
+(** [core::option::Option::{0}::unwrap] *)
+val core_option_option_unwrap_fwd
+  (t : Type0) : option t -> state -> result (state & t)
+
-- 
cgit v1.2.3