diff options
Diffstat (limited to 'tests/lean/Hashmap')
| -rw-r--r-- | tests/lean/Hashmap/Funs.lean | 8 | ||||
| -rw-r--r-- | tests/lean/Hashmap/Properties.lean | 3 |
2 files changed, 9 insertions, 2 deletions
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 [*] |