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