diff options
author | Son Ho | 2023-05-09 10:40:19 +0200 |
---|---|---|
committer | Son HO | 2023-06-04 21:44:33 +0200 |
commit | 50d1542f830b7ceb73efd34573b6b56b4971a114 (patch) | |
tree | c73b6c415b39cdbc3d92ec3056a2521445ff8afc /tests/lean/betree/BetreeMain/Opaque.lean | |
parent | 4078f2569b362920a648622be73761cddde8a288 (diff) |
Regenerate the translated files for Lean
Diffstat (limited to '')
-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) - |