diff options
Diffstat (limited to 'tests/coq/betree')
| -rw-r--r-- | tests/coq/betree/Betree_Funs.v (renamed from tests/coq/betree/BetreeMain_Funs.v) | 92 | ||||
| -rw-r--r-- | tests/coq/betree/Betree_FunsExternal.v (renamed from tests/coq/betree/BetreeMain_FunsExternal.v) | 8 | ||||
| -rw-r--r-- | tests/coq/betree/Betree_FunsExternal_Template.v (renamed from tests/coq/betree/BetreeMain_FunsExternal_Template.v) | 18 | ||||
| -rw-r--r-- | tests/coq/betree/Betree_Types.v (renamed from tests/coq/betree/BetreeMain_Types.v) | 28 | ||||
| -rw-r--r-- | tests/coq/betree/Betree_TypesExternal.v (renamed from tests/coq/betree/BetreeMain_TypesExternal.v) | 4 | ||||
| -rw-r--r-- | tests/coq/betree/Betree_TypesExternal_Template.v (renamed from tests/coq/betree/BetreeMain_TypesExternal_Template.v) | 6 | ||||
| -rw-r--r-- | tests/coq/betree/_CoqProject | 12 |
7 files changed, 84 insertions, 84 deletions
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/Betree_Funs.v index e0a1d8a2..b965d423 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/Betree_Funs.v @@ -1,18 +1,18 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: function definitions *) +(** [betree]: function definitions *) Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. -Require Import BetreeMain_Types. -Include BetreeMain_Types. -Require Import BetreeMain_FunsExternal. -Include BetreeMain_FunsExternal. -Module BetreeMain_Funs. +Require Import Betree_Types. +Include Betree_Types. +Require Import Betree_FunsExternal. +Include Betree_FunsExternal. +Module Betree_Funs. -(** [betree_main::betree::load_internal_node]: +(** [betree::betree::load_internal_node]: Source: 'src/betree.rs', lines 36:0-36:52 *) Definition betree_load_internal_node (id : u64) (st : state) : @@ -21,7 +21,7 @@ Definition betree_load_internal_node betree_utils_load_internal_node id st . -(** [betree_main::betree::store_internal_node]: +(** [betree::betree::store_internal_node]: Source: 'src/betree.rs', lines 41:0-41:60 *) Definition betree_store_internal_node (id : u64) (content : betree_List_t (u64 * betree_Message_t)) (st : state) : @@ -30,14 +30,14 @@ Definition betree_store_internal_node betree_utils_store_internal_node id content st . -(** [betree_main::betree::load_leaf_node]: +(** [betree::betree::load_leaf_node]: Source: 'src/betree.rs', lines 46:0-46:44 *) Definition betree_load_leaf_node (id : u64) (st : state) : result (state * (betree_List_t (u64 * u64))) := betree_utils_load_leaf_node id st . -(** [betree_main::betree::store_leaf_node]: +(** [betree::betree::store_leaf_node]: Source: 'src/betree.rs', lines 51:0-51:52 *) Definition betree_store_leaf_node (id : u64) (content : betree_List_t (u64 * u64)) (st : state) : @@ -46,19 +46,19 @@ Definition betree_store_leaf_node betree_utils_store_leaf_node id content st . -(** [betree_main::betree::fresh_node_id]: +(** [betree::betree::fresh_node_id]: Source: 'src/betree.rs', lines 55:0-55:48 *) Definition betree_fresh_node_id (counter : u64) : result (u64 * u64) := counter1 <- u64_add counter 1%u64; Ok (counter, counter1) . -(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: +(** [betree::betree::{betree::betree::NodeIdCounter}::new]: Source: 'src/betree.rs', lines 206:4-206:20 *) Definition betree_NodeIdCounter_new : result betree_NodeIdCounter_t := Ok {| betree_NodeIdCounter_next_node_id := 0%u64 |} . -(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: +(** [betree::betree::{betree::betree::NodeIdCounter}::fresh_id]: Source: 'src/betree.rs', lines 210:4-210:36 *) Definition betree_NodeIdCounter_fresh_id (self : betree_NodeIdCounter_t) : result (u64 * betree_NodeIdCounter_t) := @@ -67,7 +67,7 @@ Definition betree_NodeIdCounter_fresh_id {| betree_NodeIdCounter_next_node_id := i |}) . -(** [betree_main::betree::upsert_update]: +(** [betree::betree::upsert_update]: Source: 'src/betree.rs', lines 234:0-234:70 *) Definition betree_upsert_update (prev : option u64) (st : betree_UpsertFunState_t) : result u64 := @@ -88,7 +88,7 @@ Definition betree_upsert_update end . -(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: +(** [betree::betree::{betree::betree::List<T>#1}::len]: Source: 'src/betree.rs', lines 276:4-276:24 *) Fixpoint betree_List_len (T : Type) (n : nat) (self : betree_List_t T) : result u64 := @@ -102,7 +102,7 @@ Fixpoint betree_List_len end . -(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: +(** [betree::betree::{betree::betree::List<T>#1}::split_at]: Source: 'src/betree.rs', lines 284:4-284:51 *) Fixpoint betree_List_split_at (T : Type) (n : nat) (self : betree_List_t T) (n1 : u64) : @@ -125,7 +125,7 @@ Fixpoint betree_List_split_at end . -(** [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: +(** [betree::betree::{betree::betree::List<T>#1}::push_front]: Source: 'src/betree.rs', lines 299:4-299:34 *) Definition betree_List_push_front (T : Type) (self : betree_List_t T) (x : T) : result (betree_List_t T) := @@ -133,7 +133,7 @@ Definition betree_List_push_front Ok (Betree_List_Cons x tl) . -(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: +(** [betree::betree::{betree::betree::List<T>#1}::pop_front]: Source: 'src/betree.rs', lines 306:4-306:32 *) Definition betree_List_pop_front (T : Type) (self : betree_List_t T) : result (T * (betree_List_t T)) := @@ -144,7 +144,7 @@ Definition betree_List_pop_front end . -(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: +(** [betree::betree::{betree::betree::List<T>#1}::hd]: Source: 'src/betree.rs', lines 318:4-318:22 *) Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T := match self with @@ -153,7 +153,7 @@ Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T := end . -(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]: Source: 'src/betree.rs', lines 327:4-327:44 *) Definition betree_ListPairU64T_head_has_key (T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool := @@ -163,7 +163,7 @@ Definition betree_ListPairU64T_head_has_key end . -(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: Source: 'src/betree.rs', lines 339:4-339:73 *) Fixpoint betree_ListPairU64T_partition_at_pivot (T : Type) (n : nat) (self : betree_List_t (u64 * T)) (pivot : u64) : @@ -186,7 +186,7 @@ Fixpoint betree_ListPairU64T_partition_at_pivot end . -(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: +(** [betree::betree::{betree::betree::Leaf#3}::split]: Source: 'src/betree.rs', lines 359:4-364:17 *) Definition betree_Leaf_split (n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64)) @@ -222,7 +222,7 @@ Definition betree_Leaf_split node_id_cnt2)) . -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: Source: 'src/betree.rs', lines 789:4-792:34 *) Fixpoint betree_Node_lookup_first_message_for_key (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : @@ -250,7 +250,7 @@ Fixpoint betree_Node_lookup_first_message_for_key end . -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: +(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: Source: 'src/betree.rs', lines 636:4-636:80 *) Fixpoint betree_Node_lookup_in_bindings (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : @@ -271,7 +271,7 @@ Fixpoint betree_Node_lookup_in_bindings end . -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: +(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: Source: 'src/betree.rs', lines 819:4-819:90 *) Fixpoint betree_Node_apply_upserts (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64) @@ -303,7 +303,7 @@ Fixpoint betree_Node_apply_upserts end . -(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: +(** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 395:4-395:63 *) Fixpoint betree_Internal_lookup_in_children (n : nat) (self : betree_Internal_t) (key : u64) (st : state) : @@ -327,7 +327,7 @@ Fixpoint betree_Internal_lookup_in_children self.(betree_Internal_pivot) self.(betree_Internal_left) n2))) end -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: +(** [betree::betree::{betree::betree::Node#5}::lookup]: Source: 'src/betree.rs', lines 709:4-709:58 *) with betree_Node_lookup (n : nat) (self : betree_Node_t) (key : u64) (st : state) : @@ -394,7 +394,7 @@ with betree_Node_lookup end . -(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: +(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: Source: 'src/betree.rs', lines 674:4-674:77 *) Fixpoint betree_Node_filter_messages_for_key (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : @@ -419,7 +419,7 @@ Fixpoint betree_Node_filter_messages_for_key end . -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: Source: 'src/betree.rs', lines 689:4-692:34 *) Fixpoint betree_Node_lookup_first_message_after_key (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : @@ -447,7 +447,7 @@ Fixpoint betree_Node_lookup_first_message_after_key end . -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: +(** [betree::betree::{betree::betree::Node#5}::apply_to_internal]: Source: 'src/betree.rs', lines 521:4-521:89 *) Definition betree_Node_apply_to_internal (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (key : u64) @@ -508,7 +508,7 @@ Definition betree_Node_apply_to_internal lookup_first_message_for_key_back msgs2) . -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: Source: 'src/betree.rs', lines 502:4-505:5 *) Fixpoint betree_Node_apply_messages_to_internal (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) @@ -528,7 +528,7 @@ Fixpoint betree_Node_apply_messages_to_internal end . -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: +(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: Source: 'src/betree.rs', lines 653:4-656:32 *) Fixpoint betree_Node_lookup_mut_in_bindings (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : @@ -556,7 +556,7 @@ Fixpoint betree_Node_lookup_mut_in_bindings end . -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: +(** [betree::betree::{betree::betree::Node#5}::apply_to_leaf]: Source: 'src/betree.rs', lines 460:4-460:87 *) Definition betree_Node_apply_to_leaf (n : nat) (bindings : betree_List_t (u64 * u64)) (key : u64) @@ -594,7 +594,7 @@ Definition betree_Node_apply_to_leaf end . -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: Source: 'src/betree.rs', lines 444:4-447:5 *) Fixpoint betree_Node_apply_messages_to_leaf (n : nat) (bindings : betree_List_t (u64 * u64)) @@ -614,7 +614,7 @@ Fixpoint betree_Node_apply_messages_to_leaf end . -(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: +(** [betree::betree::{betree::betree::Internal#4}::flush]: Source: 'src/betree.rs', lines 410:4-415:26 *) Fixpoint betree_Internal_flush (n : nat) (self : betree_Internal_t) (params : betree_Params_t) @@ -664,7 +664,7 @@ Fixpoint betree_Internal_flush node_id_cnt1)))) end -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: +(** [betree::betree::{betree::betree::Node#5}::apply_messages]: Source: 'src/betree.rs', lines 588:4-593:5 *) with betree_Node_apply_messages (n : nat) (self : betree_Node_t) (params : betree_Params_t) @@ -720,7 +720,7 @@ with betree_Node_apply_messages end . -(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: +(** [betree::betree::{betree::betree::Node#5}::apply]: Source: 'src/betree.rs', lines 576:4-582:5 *) Definition betree_Node_apply (n : nat) (self : betree_Node_t) (params : betree_Params_t) @@ -736,7 +736,7 @@ Definition betree_Node_apply Ok (st1, (self1, node_id_cnt1)) . -(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: +(** [betree::betree::{betree::betree::BeTree#6}::new]: Source: 'src/betree.rs', lines 849:4-849:60 *) Definition betree_BeTree_new (min_flush_size : u64) (split_size : u64) (st : state) : @@ -761,7 +761,7 @@ Definition betree_BeTree_new |}) . -(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: +(** [betree::betree::{betree::betree::BeTree#6}::apply]: Source: 'src/betree.rs', lines 868:4-868:47 *) Definition betree_BeTree_apply (n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) @@ -781,7 +781,7 @@ Definition betree_BeTree_apply |}) . -(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: +(** [betree::betree::{betree::betree::BeTree#6}::insert]: Source: 'src/betree.rs', lines 874:4-874:52 *) Definition betree_BeTree_insert (n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : @@ -790,7 +790,7 @@ Definition betree_BeTree_insert betree_BeTree_apply n self key (Betree_Message_Insert value) st . -(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: +(** [betree::betree::{betree::betree::BeTree#6}::delete]: Source: 'src/betree.rs', lines 880:4-880:38 *) Definition betree_BeTree_delete (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : @@ -799,7 +799,7 @@ Definition betree_BeTree_delete betree_BeTree_apply n self key Betree_Message_Delete st . -(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: +(** [betree::betree::{betree::betree::BeTree#6}::upsert]: Source: 'src/betree.rs', lines 886:4-886:59 *) Definition betree_BeTree_upsert (n : nat) (self : betree_BeTree_t) (key : u64) @@ -809,7 +809,7 @@ Definition betree_BeTree_upsert betree_BeTree_apply n self key (Betree_Message_Upsert upd) st . -(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: +(** [betree::betree::{betree::betree::BeTree#6}::lookup]: Source: 'src/betree.rs', lines 895:4-895:62 *) Definition betree_BeTree_lookup (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : @@ -826,12 +826,12 @@ Definition betree_BeTree_lookup |})) . -(** [betree_main::main]: +(** [betree::main]: Source: 'src/main.rs', lines 4:0-4:9 *) Definition main : result unit := Ok tt. -(** Unit test for [betree_main::main] *) +(** Unit test for [betree::main] *) Check (main )%return. -End BetreeMain_Funs. +End Betree_Funs. diff --git a/tests/coq/betree/BetreeMain_FunsExternal.v b/tests/coq/betree/Betree_FunsExternal.v index 099a2e8f..0263c272 100644 --- a/tests/coq/betree/BetreeMain_FunsExternal.v +++ b/tests/coq/betree/Betree_FunsExternal.v @@ -6,9 +6,9 @@ Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. -Require Export BetreeMain_Types. -Import BetreeMain_Types. -Module BetreeMain_FunsExternal. +Require Export Betree_Types. +Import Betree_Types. +Module Betree_FunsExternal. (** [betree_main::betree_utils::load_internal_node]: forward function Source: 'src/betree_utils.rs', lines 98:0-98:63 *) @@ -36,4 +36,4 @@ Axiom betree_utils_store_leaf_node : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit) . -End BetreeMain_FunsExternal. +End Betree_FunsExternal. diff --git a/tests/coq/betree/BetreeMain_FunsExternal_Template.v b/tests/coq/betree/Betree_FunsExternal_Template.v index 58be2733..2a2fddfc 100644 --- a/tests/coq/betree/BetreeMain_FunsExternal_Template.v +++ b/tests/coq/betree/Betree_FunsExternal_Template.v @@ -1,5 +1,5 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: external functions. +(** [betree]: external functions. -- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *) Require Import Primitives. Import Primitives. @@ -7,17 +7,17 @@ Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. -Require Import BetreeMain_Types. -Include BetreeMain_Types. -Module BetreeMain_FunsExternal_Template. +Require Import Betree_Types. +Include Betree_Types. +Module Betree_FunsExternal_Template. -(** [betree_main::betree_utils::load_internal_node]: +(** [betree::betree_utils::load_internal_node]: Source: 'src/betree_utils.rs', lines 98:0-98:63 *) Axiom betree_utils_load_internal_node : u64 -> state -> result (state * (betree_List_t (u64 * betree_Message_t))) . -(** [betree_main::betree_utils::store_internal_node]: +(** [betree::betree_utils::store_internal_node]: Source: 'src/betree_utils.rs', lines 115:0-115:71 *) Axiom betree_utils_store_internal_node : @@ -25,16 +25,16 @@ Axiom betree_utils_store_internal_node unit) . -(** [betree_main::betree_utils::load_leaf_node]: +(** [betree::betree_utils::load_leaf_node]: Source: 'src/betree_utils.rs', lines 132:0-132:55 *) Axiom betree_utils_load_leaf_node : u64 -> state -> result (state * (betree_List_t (u64 * u64))) . -(** [betree_main::betree_utils::store_leaf_node]: +(** [betree::betree_utils::store_leaf_node]: Source: 'src/betree_utils.rs', lines 145:0-145:63 *) Axiom betree_utils_store_leaf_node : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit) . -End BetreeMain_FunsExternal_Template. +End Betree_FunsExternal_Template. diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/Betree_Types.v index acbc2085..aa39d8e4 100644 --- a/tests/coq/betree/BetreeMain_Types.v +++ b/tests/coq/betree/Betree_Types.v @@ -1,16 +1,16 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: type definitions *) +(** [betree]: type definitions *) Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. -Require Import BetreeMain_TypesExternal. -Include BetreeMain_TypesExternal. -Module BetreeMain_Types. +Require Import Betree_TypesExternal. +Include Betree_TypesExternal. +Module Betree_Types. -(** [betree_main::betree::List] +(** [betree::betree::List] Source: 'src/betree.rs', lines 17:0-17:23 *) Inductive betree_List_t (T : Type) := | Betree_List_Cons : T -> betree_List_t T -> betree_List_t T @@ -20,14 +20,14 @@ Inductive betree_List_t (T : Type) := Arguments Betree_List_Cons { _ }. Arguments Betree_List_Nil { _ }. -(** [betree_main::betree::UpsertFunState] +(** [betree::betree::UpsertFunState] Source: 'src/betree.rs', lines 63:0-63:23 *) Inductive betree_UpsertFunState_t := | Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t | Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t . -(** [betree_main::betree::Message] +(** [betree::betree::Message] Source: 'src/betree.rs', lines 69:0-69:23 *) Inductive betree_Message_t := | Betree_Message_Insert : u64 -> betree_Message_t @@ -35,7 +35,7 @@ Inductive betree_Message_t := | Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t . -(** [betree_main::betree::Leaf] +(** [betree::betree::Leaf] Source: 'src/betree.rs', lines 167:0-167:11 *) Record betree_Leaf_t := mkbetree_Leaf_t { @@ -43,7 +43,7 @@ mkbetree_Leaf_t { } . -(** [betree_main::betree::Internal] +(** [betree::betree::Internal] Source: 'src/betree.rs', lines 156:0-156:15 *) Inductive betree_Internal_t := | mkbetree_Internal_t : @@ -53,7 +53,7 @@ Inductive betree_Internal_t := betree_Node_t -> betree_Internal_t -(** [betree_main::betree::Node] +(** [betree::betree::Node] Source: 'src/betree.rs', lines 179:0-179:9 *) with betree_Node_t := | Betree_Node_Internal : betree_Internal_t -> betree_Node_t @@ -89,7 +89,7 @@ Notation "x2 .(betree_Internal_right)" := (betree_Internal_right x2) (at level 9) . -(** [betree_main::betree::Params] +(** [betree::betree::Params] Source: 'src/betree.rs', lines 187:0-187:13 *) Record betree_Params_t := mkbetree_Params_t { @@ -97,7 +97,7 @@ mkbetree_Params_t { } . -(** [betree_main::betree::NodeIdCounter] +(** [betree::betree::NodeIdCounter] Source: 'src/betree.rs', lines 201:0-201:20 *) Record betree_NodeIdCounter_t := mkbetree_NodeIdCounter_t { @@ -105,7 +105,7 @@ mkbetree_NodeIdCounter_t { } . -(** [betree_main::betree::BeTree] +(** [betree::betree::BeTree] Source: 'src/betree.rs', lines 218:0-218:17 *) Record betree_BeTree_t := mkbetree_BeTree_t { @@ -115,4 +115,4 @@ mkbetree_BeTree_t { } . -End BetreeMain_Types. +End Betree_Types. diff --git a/tests/coq/betree/BetreeMain_TypesExternal.v b/tests/coq/betree/Betree_TypesExternal.v index 870d2601..37487d6d 100644 --- a/tests/coq/betree/BetreeMain_TypesExternal.v +++ b/tests/coq/betree/Betree_TypesExternal.v @@ -6,9 +6,9 @@ Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. -Module BetreeMain_TypesExternal. +Module Betree_TypesExternal. (** The state type used in the state-error monad *) Axiom state : Type. -End BetreeMain_TypesExternal. +End Betree_TypesExternal. diff --git a/tests/coq/betree/BetreeMain_TypesExternal_Template.v b/tests/coq/betree/Betree_TypesExternal_Template.v index 651de2b7..a40811cb 100644 --- a/tests/coq/betree/BetreeMain_TypesExternal_Template.v +++ b/tests/coq/betree/Betree_TypesExternal_Template.v @@ -1,5 +1,5 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: external types. +(** [betree]: external types. -- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) Require Import Primitives. Import Primitives. @@ -7,9 +7,9 @@ Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. -Module BetreeMain_TypesExternal_Template. +Module Betree_TypesExternal_Template. (** The state type used in the state-error monad *) Axiom state : Type. -End BetreeMain_TypesExternal_Template. +End Betree_TypesExternal_Template. diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject index b14bed66..9fb7fe64 100644 --- a/tests/coq/betree/_CoqProject +++ b/tests/coq/betree/_CoqProject @@ -3,10 +3,10 @@ -arg -w -arg all -BetreeMain_TypesExternal_Template.v -BetreeMain_Types.v +Betree_TypesExternal_Template.v +Betree_Types.v Primitives.v -BetreeMain_FunsExternal_Template.v -BetreeMain_Funs.v -BetreeMain_TypesExternal.v -BetreeMain_FunsExternal.v +Betree_FunsExternal_Template.v +Betree_Funs.v +Betree_TypesExternal.v +Betree_FunsExternal.v |