Update the tests

6 files changed, 31 insertions, 4 deletions

diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean
index 7d8b4714..05341b31 100644
--- a/tests/lean/Betree/Funs.lean
+++ b/tests/lean/Betree/Funs.lean
@@ -248,6 +248,7 @@ divergent def betree.Node.lookup_first_message_for_key_loop
 
 /- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
    Source: 'src/betree.rs', lines 792:4-795:34 -/
+@[reducible]
 def betree.Node.lookup_first_message_for_key
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
   Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
@@ -272,6 +273,7 @@ divergent def betree.Node.lookup_in_bindings_loop
 
 /- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
    Source: 'src/betree.rs', lines 649:4-649:84 -/
+@[reducible]
 def betree.Node.lookup_in_bindings
   (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
   betree.Node.lookup_in_bindings_loop key bindings
@@ -307,6 +309,7 @@ divergent def betree.Node.apply_upserts_loop
 
 /- [betree::betree::{betree::betree::Node#5}::apply_upserts]:
    Source: 'src/betree.rs', lines 820:4-820:94 -/
+@[reducible]
 def betree.Node.apply_upserts
   (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
   :
@@ -411,6 +414,7 @@ divergent def betree.Node.filter_messages_for_key_loop
 
 /- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
    Source: 'src/betree.rs', lines 683:4-683:77 -/
+@[reducible]
 def betree.Node.filter_messages_for_key
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
   Result (betree.List (U64 × betree.Message))
@@ -443,6 +447,7 @@ divergent def betree.Node.lookup_first_message_after_key_loop
 
 /- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
    Source: 'src/betree.rs', lines 694:4-697:34 -/
+@[reducible]
 def betree.Node.lookup_first_message_after_key
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
   Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
@@ -531,6 +536,7 @@ divergent def betree.Node.apply_messages_to_internal_loop
 
 /- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
    Source: 'src/betree.rs', lines 518:4-521:5 -/
+@[reducible]
 def betree.Node.apply_messages_to_internal
   (msgs : betree.List (U64 × betree.Message))
   (new_msgs : betree.List (U64 × betree.Message)) :
@@ -563,6 +569,7 @@ divergent def betree.Node.lookup_mut_in_bindings_loop
 
 /- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
    Source: 'src/betree.rs', lines 664:4-667:32 -/
+@[reducible]
 def betree.Node.lookup_mut_in_bindings
   (key : U64) (bindings : betree.List (U64 × U64)) :
   Result ((betree.List (U64 × U64)) × (betree.List (U64 × U64) → Result
@@ -627,6 +634,7 @@ divergent def betree.Node.apply_messages_to_leaf_loop
 
 /- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
    Source: 'src/betree.rs', lines 463:4-466:5 -/
+@[reducible]
 def betree.Node.apply_messages_to_leaf
   (bindings : betree.List (U64 × U64))
   (new_msgs : betree.List (U64 × betree.Message)) :
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 48ac2062..2bbc385d 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -112,6 +112,7 @@ divergent def list_nth_mut1_loop
 
 /- [demo::list_nth_mut1]:
    Source: 'tests/src/demo.rs', lines 71:0-71:77 -/
+@[reducible]
 def list_nth_mut1
   (T : Type) (l : CList T) (i : U32) :
   Result (T × (T → Result (CList T)))
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 7d8f73a7..f5d028db 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -28,6 +28,7 @@ divergent def HashMap.allocate_slots_loop
 
 /- [hashmap::{hashmap::HashMap<T>}::allocate_slots]:
    Source: 'tests/src/hashmap.rs', lines 61:4-61:78 -/
+@[reducible]
 def HashMap.allocate_slots
   (T : Type) (slots : alloc.vec.Vec (AList T)) (n : Usize) :
   Result (alloc.vec.Vec (AList T))
@@ -106,6 +107,7 @@ divergent def HashMap.insert_in_list_loop
 
 /- [hashmap::{hashmap::HashMap<T>}::insert_in_list]:
    Source: 'tests/src/hashmap.rs', lines 108:4-108:72 -/
+@[reducible]
 def HashMap.insert_in_list
   (T : Type) (key : Usize) (value : T) (ls : AList T) :
   Result (Bool × (AList T))
@@ -150,6 +152,7 @@ divergent def HashMap.move_elements_from_list_loop
 
 /- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]:
    Source: 'tests/src/hashmap.rs', lines 194:4-194:73 -/
+@[reducible]
 def HashMap.move_elements_from_list
   (T : Type) (ntable : HashMap T) (ls : AList T) : Result (HashMap T) :=
   HashMap.move_elements_from_list_loop T ntable ls
@@ -177,6 +180,7 @@ divergent def HashMap.move_elements_loop
 
 /- [hashmap::{hashmap::HashMap<T>}::move_elements]:
    Source: 'tests/src/hashmap.rs', lines 182:4-182:96 -/
+@[reducible]
 def HashMap.move_elements
   (T : Type) (ntable : HashMap T) (slots : alloc.vec.Vec (AList T)) (i : Usize)
   :
@@ -234,6 +238,7 @@ divergent def HashMap.contains_key_in_list_loop
 
 /- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]:
    Source: 'tests/src/hashmap.rs', lines 217:4-217:69 -/
+@[reducible]
 def HashMap.contains_key_in_list
   (T : Type) (key : Usize) (ls : AList T) : Result Bool :=
   HashMap.contains_key_in_list_loop T key ls
@@ -265,6 +270,7 @@ divergent def HashMap.get_in_list_loop
 
 /- [hashmap::{hashmap::HashMap<T>}::get_in_list]:
    Source: 'tests/src/hashmap.rs', lines 235:4-235:71 -/
+@[reducible]
 def HashMap.get_in_list (T : Type) (key : Usize) (ls : AList T) : Result T :=
   HashMap.get_in_list_loop T key ls
 
@@ -306,6 +312,7 @@ divergent def HashMap.get_mut_in_list_loop
 
 /- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]:
    Source: 'tests/src/hashmap.rs', lines 256:4-256:87 -/
+@[reducible]
 def HashMap.get_mut_in_list
   (T : Type) (ls : AList T) (key : Usize) :
   Result (T × (T → Result (AList T)))
@@ -356,6 +363,7 @@ divergent def HashMap.remove_from_list_loop
 
 /- [hashmap::{hashmap::HashMap<T>}::remove_from_list]:
    Source: 'tests/src/hashmap.rs', lines 276:4-276:70 -/
+@[reducible]
 def HashMap.remove_from_list
   (T : Type) (key : Usize) (ls : AList T) : Result ((Option T) × (AList T)) :=
   HashMap.remove_from_list_loop T key ls
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index a2fa0d7d..29b5834b 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -165,8 +165,7 @@ theorem insert_in_list_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) (
        have : distinct_keys (AList.v tl0) := by
          simp [distinct_keys] at hdk
          simp [hdk, distinct_keys]
-       progress keep heq as ⟨ b, tl1 .. ⟩
-       simp only [insert_in_list] at heq
+       progress as ⟨ b, tl1 .. ⟩
        have : slot_s_inv_hash l (hash_mod_key key l) (AList.v (AList.Cons k v tl1)) := by
          simp [AList.v, slot_s_inv_hash] at *
          simp [*]
diff --git a/tests/lean/InfiniteLoop.lean b/tests/lean/InfiniteLoop.lean
index 9eb8e22c..b8c2343e 100644
--- a/tests/lean/InfiniteLoop.lean
+++ b/tests/lean/InfiniteLoop.lean
@@ -19,7 +19,7 @@ divergent def foo_loop : Result Unit :=
 
 /- [infinite_loop::foo]:
    Source: 'tests/src/infinite-loop.rs', lines 6:0-6:8 -/
-def foo : Result Unit :=
-  foo_loop
+@[reducible] def foo : Result Unit :=
+               foo_loop
 
 end infinite_loop
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 199605d5..a9e5a499 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -110,6 +110,7 @@ divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool :=
 
 /- [loops::list_mem]:
    Source: 'tests/src/loops.rs', lines 80:0-80:52 -/
+@[reducible]
 def list_mem (x : U32) (ls : List U32) : Result Bool :=
   list_mem_loop x ls
 
@@ -136,6 +137,7 @@ divergent def list_nth_mut_loop_loop
 
 /- [loops::list_nth_mut_loop]:
    Source: 'tests/src/loops.rs', lines 92:0-92:71 -/
+@[reducible]
 def list_nth_mut_loop
   (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
   list_nth_mut_loop_loop T ls i
@@ -155,6 +157,7 @@ divergent def list_nth_shared_loop_loop
 
 /- [loops::list_nth_shared_loop]:
    Source: 'tests/src/loops.rs', lines 105:0-105:66 -/
+@[reducible]
 def list_nth_shared_loop (T : Type) (ls : List T) (i : U32) : Result T :=
   list_nth_shared_loop_loop T ls i
 
@@ -316,6 +319,7 @@ divergent def list_nth_mut_loop_pair_loop
 
 /- [loops::list_nth_mut_loop_pair]:
    Source: 'tests/src/loops.rs', lines 188:0-192:27 -/
+@[reducible]
 def list_nth_mut_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)) × (T → Result (List T)))
@@ -340,6 +344,7 @@ divergent def list_nth_shared_loop_pair_loop
 
 /- [loops::list_nth_shared_loop_pair]:
    Source: 'tests/src/loops.rs', lines 212:0-216:19 -/
+@[reducible]
 def list_nth_shared_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   list_nth_shared_loop_pair_loop T ls0 ls1 i
@@ -376,6 +381,7 @@ divergent def list_nth_mut_loop_pair_merge_loop
 
 /- [loops::list_nth_mut_loop_pair_merge]:
    Source: 'tests/src/loops.rs', lines 237:0-241:27 -/
+@[reducible]
 def list_nth_mut_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × ((T × T) → Result ((List T) × (List T))))
@@ -401,6 +407,7 @@ divergent def list_nth_shared_loop_pair_merge_loop
 
 /- [loops::list_nth_shared_loop_pair_merge]:
    Source: 'tests/src/loops.rs', lines 255:0-259:19 -/
+@[reducible]
 def list_nth_shared_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   list_nth_shared_loop_pair_merge_loop T ls0 ls1 i
@@ -433,6 +440,7 @@ divergent def list_nth_mut_shared_loop_pair_loop
 
 /- [loops::list_nth_mut_shared_loop_pair]:
    Source: 'tests/src/loops.rs', lines 273:0-277:23 -/
+@[reducible]
 def list_nth_mut_shared_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
@@ -467,6 +475,7 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop
 
 /- [loops::list_nth_mut_shared_loop_pair_merge]:
    Source: 'tests/src/loops.rs', lines 292:0-296:23 -/
+@[reducible]
 def list_nth_mut_shared_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
@@ -501,6 +510,7 @@ divergent def list_nth_shared_mut_loop_pair_loop
 
 /- [loops::list_nth_shared_mut_loop_pair]:
    Source: 'tests/src/loops.rs', lines 311:0-315:23 -/
+@[reducible]
 def list_nth_shared_mut_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
@@ -535,6 +545,7 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop
 
 /- [loops::list_nth_shared_mut_loop_pair_merge]:
    Source: 'tests/src/loops.rs', lines 330:0-334:23 -/
+@[reducible]
 def list_nth_shared_mut_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))