diff options
Diffstat (limited to 'tests/lean/hashmap_on_disk/HashmapMain')
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index 5b7d6f46..1abc9f8d 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -110,7 +110,6 @@ def hashmap_hash_map_insert_in_list_loop_fwd then result.ret false else hashmap_hash_map_insert_in_list_loop_fwd T key value tl | hashmap_list_t.HashmapListNil => result.ret true - termination_by hashmap_hash_map_insert_in_list_loop_fwd key value ls => hashmap_hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls @@ -136,7 +135,6 @@ def hashmap_hash_map_insert_in_list_loop_back | hashmap_list_t.HashmapListNil => let l := hashmap_list_t.HashmapListNil result.ret (hashmap_list_t.HashmapListCons key value l) - termination_by hashmap_hash_map_insert_in_list_loop_back key value ls => hashmap_hash_map_insert_in_list_loop_terminates T key value ls decreasing_by hashmap_hash_map_insert_in_list_loop_decreases key value ls @@ -206,7 +204,6 @@ def hashmap_hash_map_move_elements_from_list_loop_fwd_back let ntable0 <- hashmap_hash_map_insert_no_resize_fwd_back T ntable k v hashmap_hash_map_move_elements_from_list_loop_fwd_back T ntable0 tl | hashmap_list_t.HashmapListNil => result.ret ntable - termination_by hashmap_hash_map_move_elements_from_list_loop_fwd_back ntable ls => hashmap_hash_map_move_elements_from_list_loop_terminates T ntable ls @@ -306,7 +303,6 @@ def hashmap_hash_map_contains_key_in_list_loop_fwd then result.ret true else hashmap_hash_map_contains_key_in_list_loop_fwd T key tl | hashmap_list_t.HashmapListNil => result.ret false - termination_by hashmap_hash_map_contains_key_in_list_loop_fwd key ls => hashmap_hash_map_contains_key_in_list_loop_terminates T key ls decreasing_by hashmap_hash_map_contains_key_in_list_loop_decreases key ls @@ -336,7 +332,6 @@ def hashmap_hash_map_get_in_list_loop_fwd then result.ret cvalue else hashmap_hash_map_get_in_list_loop_fwd T key tl | hashmap_list_t.HashmapListNil => result.fail error.panic - termination_by hashmap_hash_map_get_in_list_loop_fwd key ls => hashmap_hash_map_get_in_list_loop_terminates T key ls decreasing_by hashmap_hash_map_get_in_list_loop_decreases key ls @@ -366,7 +361,6 @@ def hashmap_hash_map_get_mut_in_list_loop_fwd then result.ret cvalue else hashmap_hash_map_get_mut_in_list_loop_fwd T tl key | hashmap_list_t.HashmapListNil => result.fail error.panic - termination_by hashmap_hash_map_get_mut_in_list_loop_fwd ls key => hashmap_hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key @@ -390,7 +384,6 @@ def hashmap_hash_map_get_mut_in_list_loop_back let tl0 <- hashmap_hash_map_get_mut_in_list_loop_back T tl key ret0 result.ret (hashmap_list_t.HashmapListCons ckey cvalue tl0) | hashmap_list_t.HashmapListNil => result.fail error.panic - termination_by hashmap_hash_map_get_mut_in_list_loop_back ls key ret0 => hashmap_hash_map_get_mut_in_list_loop_terminates T ls key decreasing_by hashmap_hash_map_get_mut_in_list_loop_decreases ls key @@ -450,10 +443,8 @@ def hashmap_hash_map_remove_from_list_loop_fwd | hashmap_list_t.HashmapListCons i cvalue tl0 => result.ret (Option.some cvalue) | hashmap_list_t.HashmapListNil => result.fail error.panic - else hashmap_hash_map_remove_from_list_loop_fwd T key tl | hashmap_list_t.HashmapListNil => result.ret Option.none - termination_by hashmap_hash_map_remove_from_list_loop_fwd key ls => hashmap_hash_map_remove_from_list_loop_terminates T key ls decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls @@ -478,13 +469,11 @@ def hashmap_hash_map_remove_from_list_loop_back match mv_ls with | hashmap_list_t.HashmapListCons i cvalue tl0 => result.ret tl0 | hashmap_list_t.HashmapListNil => result.fail error.panic - else do let tl0 <- hashmap_hash_map_remove_from_list_loop_back T key tl result.ret (hashmap_list_t.HashmapListCons ckey t tl0) | hashmap_list_t.HashmapListNil => result.ret hashmap_list_t.HashmapListNil - termination_by hashmap_hash_map_remove_from_list_loop_back key ls => hashmap_hash_map_remove_from_list_loop_terminates T key ls decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls @@ -513,7 +502,6 @@ def hashmap_hash_map_remove_fwd let _ <- USize.checked_sub self.hashmap_hash_map_num_entries (USize.ofNatCore 1 (by intlit)) result.ret (Option.some x0) - /- [hashmap_main::hashmap::HashMap::{0}::remove] -/ def hashmap_hash_map_remove_back @@ -556,7 +544,6 @@ def hashmap_hash_map_remove_back hashmap_hash_map_max_load := self.hashmap_hash_map_max_load, hashmap_hash_map_slots := v } - /- [hashmap_main::hashmap::test1] -/ def hashmap_test1_fwd : result Unit := @@ -624,7 +611,6 @@ def hashmap_test1_fwd : result Unit := if not (i3 = (UInt64.ofNatCore 256 (by intlit))) then result.fail error.panic else result.ret () - /- Unit test for [hashmap_main::hashmap::test1] -/ #assert (hashmap_test1_fwd = .ret ()) |