diff options
author | Son Ho | 2023-02-05 18:48:11 +0100 |
---|---|---|
committer | Son HO | 2023-06-04 21:44:33 +0200 |
commit | 9ec68c058a1829166fbb2511dedfbe0c2f94d6bc (patch) | |
tree | 39e08e0e2471d9e27d2bdc1fdd61e74801345383 /tests/lean/hashmap_on_disk/HashmapMain | |
parent | 985abfa5406e55a8a4e091486119e18b60896911 (diff) |
Improve formatting of the termination_by clauses
Diffstat (limited to 'tests/lean/hashmap_on_disk/HashmapMain')
-rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Funs.lean | 32 |
1 files changed, 13 insertions, 19 deletions
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean index 5134f483..2795ecfa 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean @@ -24,8 +24,7 @@ def hashmap_hash_map_allocate_slots_loop_fwd hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0 else result.ret slots termination_by hashmap_hash_map_allocate_slots_loop_fwd slots n => - hashmap_hash_map_allocate_slots_loop_terminates - T slots n + hashmap_hash_map_allocate_slots_loop_terminates T slots n decreasing_by hashmap_hash_map_allocate_slots_loop_decreases slots n /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/ @@ -76,8 +75,7 @@ def hashmap_hash_map_clear_loop_fwd_back hashmap_hash_map_clear_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 + hashmap_hash_map_clear_loop_terminates T slots i decreasing_by hashmap_hash_map_clear_loop_decreases slots i /- [hashmap_main::hashmap::HashMap::{0}::clear] -/ @@ -113,7 +111,7 @@ def hashmap_hash_map_insert_in_list_loop_fwd | 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 + 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 /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ @@ -139,7 +137,7 @@ def hashmap_hash_map_insert_in_list_loop_back 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 + 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 /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/ @@ -209,8 +207,8 @@ def hashmap_hash_map_move_elements_from_list_loop_fwd_back | 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 + => + hashmap_hash_map_move_elements_from_list_loop_terminates T ntable ls decreasing_by hashmap_hash_map_move_elements_from_list_loop_decreases ntable ls /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] -/ @@ -242,7 +240,7 @@ def hashmap_hash_map_move_elements_loop_fwd_back hashmap_hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1 else result.ret (ntable, slots) termination_by hashmap_hash_map_move_elements_loop_fwd_back ntable slots i => - hashmap_hash_map_move_elements_loop_terminates T ntable slots i + hashmap_hash_map_move_elements_loop_terminates T ntable slots i decreasing_by hashmap_hash_map_move_elements_loop_decreases ntable slots i /- [hashmap_main::hashmap::HashMap::{0}::move_elements] -/ @@ -309,7 +307,7 @@ def hashmap_hash_map_contains_key_in_list_loop_fwd | 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 + 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 /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/ @@ -339,8 +337,7 @@ def hashmap_hash_map_get_in_list_loop_fwd | 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 + hashmap_hash_map_get_in_list_loop_terminates T key ls decreasing_by hashmap_hash_map_get_in_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/ @@ -370,8 +367,7 @@ def hashmap_hash_map_get_mut_in_list_loop_fwd | 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 + 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 /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ @@ -395,7 +391,7 @@ def hashmap_hash_map_get_mut_in_list_loop_back | 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 + 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 /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/ @@ -458,8 +454,7 @@ def hashmap_hash_map_remove_from_list_loop_fwd | 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 + hashmap_hash_map_remove_from_list_loop_terminates T key ls decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ @@ -490,8 +485,7 @@ def hashmap_hash_map_remove_from_list_loop_back | 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 + hashmap_hash_map_remove_from_list_loop_terminates T key ls decreasing_by hashmap_hash_map_remove_from_list_loop_decreases key ls /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/ |