1 files changed, 0 insertions, 185 deletions
diff --git a/tests/lean/betree/BetreeMain/Clauses/Template.lean b/tests/lean/betree/BetreeMain/Clauses/Template.lean
deleted file mode 100644
index 1d18174e..00000000
--- a/tests/lean/betree/BetreeMain/Clauses/Template.lean
+++ /dev/null
@@ -1,185 +0,0 @@
--- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [betree_main]: templates for the decreases clauses
-import Base.Primitives
-import BetreeMain.Types
-
-/- [betree_main::betree::List::{1}::len]: termination measure -/
-@[simp]
-def betree_list_len_terminates (T : Type) (self : betree_list_t T) := self
-
-/- [betree_main::betree::List::{1}::len]: decreases_by tactic -/
-syntax "betree_list_len_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_list_len_decreases $self) =>`(tactic| sorry)
-
-/- [betree_main::betree::List::{1}::split_at]: termination measure -/
-@[simp]
-def betree_list_split_at_terminates (T : Type) (self : betree_list_t T)
-  (n : UInt64) :=
-  (self, n)
-
-/- [betree_main::betree::List::{1}::split_at]: decreases_by tactic -/
-syntax "betree_list_split_at_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_list_split_at_decreases $self $n) =>`(tactic| sorry)
-
-/- [betree_main::betree::List::{2}::partition_at_pivot]: termination measure -/
-@[simp]
-def betree_list_partition_at_pivot_terminates (T : Type)
-  (self : betree_list_t (UInt64 × T)) (pivot : UInt64) :=
-  (self, pivot)
-
-/- [betree_main::betree::List::{2}::partition_at_pivot]: decreases_by tactic -/
-syntax "betree_list_partition_at_pivot_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_list_partition_at_pivot_decreases $self $pivot) =>
-  `(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::lookup_in_bindings]: termination measure -/
-@[simp]
-def betree_node_lookup_in_bindings_terminates (key : UInt64)
-  (bindings : betree_list_t (UInt64 × UInt64)) :=
-  (key, bindings)
-
-/- [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases_by tactic -/
-syntax "betree_node_lookup_in_bindings_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_lookup_in_bindings_decreases $key $bindings) =>
-  `(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::lookup_first_message_for_key]: termination measure -/
-@[simp]
-def betree_node_lookup_first_message_for_key_terminates (key : UInt64)
-  (msgs : betree_list_t (UInt64 × betree_message_t)) :=
-  (key, msgs)
-
-/- [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases_by tactic -/
-syntax "betree_node_lookup_first_message_for_key_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_lookup_first_message_for_key_decreases $key $msgs) =>
-  `(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::apply_upserts]: termination measure -/
-@[simp]
-def betree_node_apply_upserts_terminates
-  (msgs : betree_list_t (UInt64 × betree_message_t)) (prev : Option UInt64)
-  (key : UInt64) (st : State) :=
-  (msgs, prev, key, st)
-
-/- [betree_main::betree::Node::{5}::apply_upserts]: decreases_by tactic -/
-syntax "betree_node_apply_upserts_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_apply_upserts_decreases $msgs $prev $key $st) =>
-  `(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::lookup]: termination measure -/
-@[simp]
-def betree_node_lookup_terminates (self : betree_node_t) (key : UInt64)
-  (st : State) :=
-  (self, key, st)
-
-/- [betree_main::betree::Node::{5}::lookup]: decreases_by tactic -/
-syntax "betree_node_lookup_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_lookup_decreases $self $key $st) =>`(tactic| sorry)
-
-/- [betree_main::betree::Internal::{4}::lookup_in_children]: termination measure -/
-@[simp]
-def betree_internal_lookup_in_children_terminates (self : betree_internal_t)
-  (key : UInt64) (st : State) :=
-  (self, key, st)
-
-/- [betree_main::betree::Internal::{4}::lookup_in_children]: decreases_by tactic -/
-syntax "betree_internal_lookup_in_children_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_internal_lookup_in_children_decreases $self $key $st) =>
-  `(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: termination measure -/
-@[simp]
-def betree_node_lookup_mut_in_bindings_terminates (key : UInt64)
-  (bindings : betree_list_t (UInt64 × UInt64)) :=
-  (key, bindings)
-
-/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases_by tactic -/
-syntax "betree_node_lookup_mut_in_bindings_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_lookup_mut_in_bindings_decreases $key $bindings) =>
-  `(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::apply_messages_to_leaf]: termination measure -/
-@[simp]
-def betree_node_apply_messages_to_leaf_terminates
-  (bindings : betree_list_t (UInt64 × UInt64))
-  (new_msgs : betree_list_t (UInt64 × betree_message_t)) :=
-  (bindings, new_msgs)
-
-/- [betree_main::betree::Node::{5}::apply_messages_to_leaf]: decreases_by tactic -/
-syntax "betree_node_apply_messages_to_leaf_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_apply_messages_to_leaf_decreases $bindings
-$new_msgs) =>`(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::filter_messages_for_key]: termination measure -/
-@[simp]
-def betree_node_filter_messages_for_key_terminates (key : UInt64)
-  (msgs : betree_list_t (UInt64 × betree_message_t)) :=
-  (key, msgs)
-
-/- [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases_by tactic -/
-syntax "betree_node_filter_messages_for_key_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_filter_messages_for_key_decreases $key $msgs) =>
-  `(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::lookup_first_message_after_key]: termination measure -/
-@[simp]
-def betree_node_lookup_first_message_after_key_terminates (key : UInt64)
-  (msgs : betree_list_t (UInt64 × betree_message_t)) :=
-  (key, msgs)
-
-/- [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases_by tactic -/
-syntax "betree_node_lookup_first_message_after_key_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_lookup_first_message_after_key_decreases $key $msgs) =>
-  `(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::apply_messages_to_internal]: termination measure -/
-@[simp]
-def betree_node_apply_messages_to_internal_terminates
-  (msgs : betree_list_t (UInt64 × betree_message_t))
-  (new_msgs : betree_list_t (UInt64 × betree_message_t)) :=
-  (msgs, new_msgs)
-
-/- [betree_main::betree::Node::{5}::apply_messages_to_internal]: decreases_by tactic -/
-syntax "betree_node_apply_messages_to_internal_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_apply_messages_to_internal_decreases $msgs
-$new_msgs) =>`(tactic| sorry)
-
-/- [betree_main::betree::Node::{5}::apply_messages]: termination measure -/
-@[simp]
-def betree_node_apply_messages_terminates (self : betree_node_t)
-  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
-  (msgs : betree_list_t (UInt64 × betree_message_t)) (st : State) :=
-  (self, params, node_id_cnt, msgs, st)
-
-/- [betree_main::betree::Node::{5}::apply_messages]: decreases_by tactic -/
-syntax "betree_node_apply_messages_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_node_apply_messages_decreases $self $params $node_id_cnt
-$msgs $st) =>`(tactic| sorry)
-
-/- [betree_main::betree::Internal::{4}::flush]: termination measure -/
-@[simp]
-def betree_internal_flush_terminates (self : betree_internal_t)
-  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
-  (content : betree_list_t (UInt64 × betree_message_t)) (st : State) :=
-  (self, params, node_id_cnt, content, st)
-
-/- [betree_main::betree::Internal::{4}::flush]: decreases_by tactic -/
-syntax "betree_internal_flush_decreases" term+ : tactic
-macro_rules
-| `(tactic| betree_internal_flush_decreases $self $params $node_id_cnt $content
-$st) =>`(tactic| sorry)
-