diff options
Diffstat (limited to 'tests/lean/BetreeMain/Opaque.lean')
-rw-r--r-- | tests/lean/BetreeMain/Opaque.lean | 35 |
1 files changed, 0 insertions, 35 deletions
diff --git a/tests/lean/BetreeMain/Opaque.lean b/tests/lean/BetreeMain/Opaque.lean deleted file mode 100644 index d043186b..00000000 --- a/tests/lean/BetreeMain/Opaque.lean +++ /dev/null @@ -1,35 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [betree_main]: opaque function definitions -import Base -import BetreeMain.Types -open Primitives - -namespace BetreeMain - -structure OpaqueDefs where - - /- [betree_main::betree_utils::load_internal_node] -/ - betree_utils_load_internal_node_fwd - : - U64 → State → Result (State × (betree_list_t (U64 × - betree_message_t))) - - /- [betree_main::betree_utils::store_internal_node] -/ - 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] -/ - betree_utils_load_leaf_node_fwd - : U64 → State → Result (State × (betree_list_t (U64 × U64))) - - /- [betree_main::betree_utils::store_leaf_node] -/ - betree_utils_store_leaf_node_fwd - : U64 → betree_list_t (U64 × U64) → State → Result (State × Unit) - - /- [core::option::Option::{0}::unwrap] -/ - core_option_option_unwrap_fwd - (T : Type) : Option T → State → Result (State × T) - -end BetreeMain |