From feb60683216a6d9193d6353605560c6c80a1ab41 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 7 Mar 2023 08:41:57 +0100
Subject: Make minor modifications and regenerate the Lean files

---
 tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'tests/lean/hashmap_on_disk/HashmapMain/Clauses')

diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean
index a514c58a..e64419a6 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Template.lean
@@ -15,17 +15,16 @@ macro_rules
 | `(tactic| hashmap_hash_map_allocate_slots_loop_decreases $slots $n) =>
   `(tactic| sorry)
 
-/- [hashmap_main::hashmap::HashMap::{0}::clear_slots]: termination measure -/
+/- [hashmap_main::hashmap::HashMap::{0}::clear]: termination measure -/
 @[simp]
-def hashmap_hash_map_clear_slots_loop_terminates (T : Type)
+def hashmap_hash_map_clear_loop_terminates (T : Type)
   (slots : Vec (hashmap_list_t T)) (i : USize) :=
   (slots, i)
 
-syntax "hashmap_hash_map_clear_slots_loop_decreases" term+ : tactic
+syntax "hashmap_hash_map_clear_loop_decreases" term+ : tactic
 
 macro_rules
-| `(tactic| hashmap_hash_map_clear_slots_loop_decreases $slots $i) =>
-  `(tactic| sorry)
+| `(tactic| hashmap_hash_map_clear_loop_decreases $slots $i) =>`(tactic| sorry)
 
 /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: termination measure -/
 @[simp]
-- 
cgit v1.2.3