diff options
author | Son Ho | 2022-11-14 14:14:38 +0100 |
---|---|---|
committer | Son HO | 2022-11-14 14:21:04 +0100 |
commit | 6f714017d71a512042b22d7d0e987f75b47a088f (patch) | |
tree | ed608a74538ff5a34a32a2aee9094e9f41979121 /tests/coq/betree/BetreeMain__Opaque.v | |
parent | 6cfd60a0d75a1fcc3734aa9729c79acbfb30e546 (diff) |
Extract the Polonius examples in Coq
Diffstat (limited to '')
-rw-r--r-- | tests/coq/betree/BetreeMain__Opaque.v | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/tests/coq/betree/BetreeMain__Opaque.v b/tests/coq/betree/BetreeMain__Opaque.v new file mode 100644 index 00000000..95d4b7c0 --- /dev/null +++ b/tests/coq/betree/BetreeMain__Opaque.v @@ -0,0 +1,38 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: opaque function definitions *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Local Open Scope Primitives_scope. +Require Export BetreeMain__Types . +Import BetreeMain__Types . +Module BetreeMain__Opaque . + +(** [betree_main::betree_utils::load_internal_node] *) +Axiom betree_utils_load_internal_node_fwd + : u64 -> state -> result (state * (Betree_list_t (u64 * Betree_message_t))) + . + +(** [betree_main::betree_utils::store_internal_node] *) +Axiom 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] *) +Axiom betree_utils_load_leaf_node_fwd + : u64 -> state -> result (state * (Betree_list_t (u64 * u64))) + . + +(** [betree_main::betree_utils::store_leaf_node] *) +Axiom betree_utils_store_leaf_node_fwd + : u64 -> Betree_list_t (u64 * u64) -> state -> result (state * unit) + . + +(** [core::option::Option::{0}::unwrap] *) +Axiom core_option_option_unwrap_fwd : + forall(T : Type) , option T -> state -> result (state * T) + . + +End BetreeMain__Opaque . |