Update the extraction of Lean files

3 files changed, 27 insertions, 18 deletions

diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean
index 16a4ea4c..a514c58a 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean
@@ -1,11 +1,12 @@
--- [hashmap_main]: decreases clauses
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [hashmap_main]: templates for the decreases clauses
 import Base.Primitives
 import HashmapMain.Types
 
 /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: termination measure -/
 @[simp]
 def hashmap_hash_map_allocate_slots_loop_terminates (T : Type)
-  (slots : vec (hashmap_list_t T)) (n : USize) :=
+  (slots : Vec (hashmap_list_t T)) (n : USize) :=
   (slots, n)
 
 syntax "hashmap_hash_map_allocate_slots_loop_decreases" term+ : tactic
@@ -14,16 +15,17 @@ macro_rules
 | `(tactic| hashmap_hash_map_allocate_slots_loop_decreases $slots $n) =>
   `(tactic| sorry)
 
-/- [hashmap_main::hashmap::HashMap::{0}::clear]: termination measure -/
+/- [hashmap_main::hashmap::HashMap::{0}::clear_slots]: termination measure -/
 @[simp]
-def hashmap_hash_map_clear_loop_terminates (T : Type)
-  (slots : vec (hashmap_list_t T)) (i : USize) :=
+def hashmap_hash_map_clear_slots_loop_terminates (T : Type)
+  (slots : Vec (hashmap_list_t T)) (i : USize) :=
   (slots, i)
 
-syntax "hashmap_hash_map_clear_loop_decreases" term+ : tactic
+syntax "hashmap_hash_map_clear_slots_loop_decreases" term+ : tactic
 
 macro_rules
-| `(tactic| hashmap_hash_map_clear_loop_decreases $slots $i) =>`(tactic| sorry)
+| `(tactic| hashmap_hash_map_clear_slots_loop_decreases $slots $i) =>
+  `(tactic| sorry)
 
 /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: termination measure -/
 @[simp]
@@ -52,7 +54,7 @@ $ls) =>`(tactic| sorry)
 /- [hashmap_main::hashmap::HashMap::{0}::move_elements]: termination measure -/
 @[simp]
 def hashmap_hash_map_move_elements_loop_terminates (T : Type)
-  (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) (i : USize)
+  (ntable : hashmap_hash_map_t T) (slots : Vec (hashmap_list_t T)) (i : USize)
   :=
   (ntable, slots, i)
 
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
index c85d14f4..392c8816 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
@@ -60,8 +60,8 @@ def hashmap_hash_map_new_fwd (T : Type) : Result (hashmap_hash_map_t T) :=
   hashmap_hash_map_new_with_capacity_fwd T (USize.ofNatCore 32 (by intlit))
     (USize.ofNatCore 4 (by intlit)) (USize.ofNatCore 5 (by intlit))
 
-/- [hashmap_main::hashmap::HashMap::{0}::clear] -/
-def hashmap_hash_map_clear_loop_fwd_back
+/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/
+def hashmap_hash_map_clear_slots_loop_fwd_back
   (T : Type) (slots : Vec (hashmap_list_t T)) (i : USize) :
   (Result (Vec (hashmap_list_t T)))
   :=
@@ -73,19 +73,26 @@ def hashmap_hash_map_clear_loop_fwd_back
       let slots0 ←
         vec_index_mut_back (hashmap_list_t T) slots i
           hashmap_list_t.HashmapListNil
-      hashmap_hash_map_clear_loop_fwd_back T slots0 i1
+      hashmap_hash_map_clear_slots_loop_fwd_back T slots0 i1
   else Result.ret slots
-termination_by hashmap_hash_map_clear_loop_fwd_back slots i =>
-  hashmap_hash_map_clear_loop_terminates T slots i
-decreasing_by hashmap_hash_map_clear_loop_decreases slots i
+termination_by hashmap_hash_map_clear_slots_loop_fwd_back slots i =>
+  hashmap_hash_map_clear_slots_loop_terminates T slots i
+decreasing_by hashmap_hash_map_clear_slots_loop_decreases slots i
+
+/- [hashmap_main::hashmap::HashMap::{0}::clear_slots] -/
+def hashmap_hash_map_clear_slots_fwd_back
+  (T : Type) (slots : Vec (hashmap_list_t T)) :
+  Result (Vec (hashmap_list_t T))
+  :=
+  hashmap_hash_map_clear_slots_loop_fwd_back T slots
+    (USize.ofNatCore 0 (by intlit))
 
 /- [hashmap_main::hashmap::HashMap::{0}::clear] -/
 def hashmap_hash_map_clear_fwd_back
   (T : Type) (self : hashmap_hash_map_t T) : Result (hashmap_hash_map_t T) :=
   do
     let v ←
-      hashmap_hash_map_clear_loop_fwd_back T self.hashmap_hash_map_slots
-        (USize.ofNatCore 0 (by intlit))
+      hashmap_hash_map_clear_slots_fwd_back T self.hashmap_hash_map_slots
     Result.ret
       {
         hashmap_hash_map_num_entries := (USize.ofNatCore 0 (by intlit)),
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean
index 40f9b7e9..fbab1bcd 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Types.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Types.lean
@@ -9,11 +9,11 @@ inductive hashmap_list_t (T : Type) :=
 
 /- [hashmap_main::hashmap::HashMap] -/
 structure hashmap_hash_map_t (T : Type) where
-
   hashmap_hash_map_num_entries : USize
   hashmap_hash_map_max_load_factor : (USize × USize)
   hashmap_hash_map_max_load : USize
   hashmap_hash_map_slots : Vec (hashmap_list_t T)
 
-/- The state type used in the state-error monad -/ axiom State : Type
+/- The state type used in the state-error monad -/
+axiom State : Type