summaryrefslogtreecommitdiff
path: root/tests/lean/hashmap
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/lean/hashmap/Hashmap/Funs.lean34
-rw-r--r--tests/lean/hashmap_on_disk/HashmapMain/Funs.lean32
2 files changed, 25 insertions, 41 deletions
diff --git a/tests/lean/hashmap/Hashmap/Funs.lean b/tests/lean/hashmap/Hashmap/Funs.lean
index 030b335a..1b03b7a2 100644
--- a/tests/lean/hashmap/Hashmap/Funs.lean
+++ b/tests/lean/hashmap/Hashmap/Funs.lean
@@ -20,8 +20,7 @@ def hash_map_allocate_slots_loop_fwd
hash_map_allocate_slots_loop_fwd T slots0 n0
else result.ret slots
termination_by hash_map_allocate_slots_loop_fwd slots n =>
- hash_map_allocate_slots_loop_terminates
- T slots n
+ hash_map_allocate_slots_loop_terminates T slots n
decreasing_by hash_map_allocate_slots_loop_decreases slots n
/- [hashmap::HashMap::{0}::allocate_slots] -/
@@ -67,8 +66,7 @@ def hash_map_clear_loop_fwd_back
hash_map_clear_loop_fwd_back T slots0 i1
else result.ret slots
termination_by hash_map_clear_loop_fwd_back slots i =>
- hash_map_clear_loop_terminates
- T slots i
+ hash_map_clear_loop_terminates T slots i
decreasing_by hash_map_clear_loop_decreases slots i
/- [hashmap::HashMap::{0}::clear] -/
@@ -101,8 +99,7 @@ def hash_map_insert_in_list_loop_fwd
| list_t.ListNil => result.ret true
termination_by hash_map_insert_in_list_loop_fwd key value ls =>
- hash_map_insert_in_list_loop_terminates
- T key value ls
+ hash_map_insert_in_list_loop_terminates T key value ls
decreasing_by hash_map_insert_in_list_loop_decreases key value ls
/- [hashmap::HashMap::{0}::insert_in_list] -/
@@ -125,8 +122,7 @@ def hash_map_insert_in_list_loop_back
let l := list_t.ListNil result.ret (list_t.ListCons key value l)
termination_by hash_map_insert_in_list_loop_back key value ls =>
- hash_map_insert_in_list_loop_terminates
- T key value ls
+ hash_map_insert_in_list_loop_terminates T key value ls
decreasing_by hash_map_insert_in_list_loop_decreases key value ls
/- [hashmap::HashMap::{0}::insert_in_list] -/
@@ -189,7 +185,7 @@ def hash_map_move_elements_from_list_loop_fwd_back
| list_t.ListNil => result.ret ntable
termination_by hash_map_move_elements_from_list_loop_fwd_back ntable ls =>
- hash_map_move_elements_from_list_loop_terminates T ntable ls
+ hash_map_move_elements_from_list_loop_terminates T ntable ls
decreasing_by hash_map_move_elements_from_list_loop_decreases ntable ls
/- [hashmap::HashMap::{0}::move_elements_from_list] -/
@@ -215,7 +211,7 @@ def hash_map_move_elements_loop_fwd_back
hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1
else result.ret (ntable, slots)
termination_by hash_map_move_elements_loop_fwd_back ntable slots i =>
- hash_map_move_elements_loop_terminates T ntable slots i
+ hash_map_move_elements_loop_terminates T ntable slots i
decreasing_by hash_map_move_elements_loop_decreases ntable slots i
/- [hashmap::HashMap::{0}::move_elements] -/
@@ -281,8 +277,7 @@ def hash_map_contains_key_in_list_loop_fwd
| list_t.ListNil => result.ret false
termination_by hash_map_contains_key_in_list_loop_fwd key ls =>
- hash_map_contains_key_in_list_loop_terminates
- T key ls
+ hash_map_contains_key_in_list_loop_terminates T key ls
decreasing_by hash_map_contains_key_in_list_loop_decreases key ls
/- [hashmap::HashMap::{0}::contains_key_in_list] -/
@@ -311,8 +306,7 @@ def hash_map_get_in_list_loop_fwd
| list_t.ListNil => result.fail error.panic
termination_by hash_map_get_in_list_loop_fwd key ls =>
- hash_map_get_in_list_loop_terminates
- T key ls
+ hash_map_get_in_list_loop_terminates T key ls
decreasing_by hash_map_get_in_list_loop_decreases key ls
/- [hashmap::HashMap::{0}::get_in_list] -/
@@ -341,8 +335,7 @@ def hash_map_get_mut_in_list_loop_fwd
| list_t.ListNil => result.fail error.panic
termination_by hash_map_get_mut_in_list_loop_fwd ls key =>
- hash_map_get_mut_in_list_loop_terminates
- T ls key
+ hash_map_get_mut_in_list_loop_terminates T ls key
decreasing_by hash_map_get_mut_in_list_loop_decreases ls key
/- [hashmap::HashMap::{0}::get_mut_in_list] -/
@@ -364,8 +357,7 @@ def hash_map_get_mut_in_list_loop_back
| list_t.ListNil => result.fail error.panic
termination_by hash_map_get_mut_in_list_loop_back ls key ret0 =>
- hash_map_get_mut_in_list_loop_terminates
- T ls key
+ hash_map_get_mut_in_list_loop_terminates T ls key
decreasing_by hash_map_get_mut_in_list_loop_decreases ls key
/- [hashmap::HashMap::{0}::get_mut_in_list] -/
@@ -420,8 +412,7 @@ def hash_map_remove_from_list_loop_fwd
| list_t.ListNil => result.ret Option.none
termination_by hash_map_remove_from_list_loop_fwd key ls =>
- hash_map_remove_from_list_loop_terminates
- T key ls
+ hash_map_remove_from_list_loop_terminates T key ls
decreasing_by hash_map_remove_from_list_loop_decreases key ls
/- [hashmap::HashMap::{0}::remove_from_list] -/
@@ -449,8 +440,7 @@ def hash_map_remove_from_list_loop_back
| list_t.ListNil => result.ret list_t.ListNil
termination_by hash_map_remove_from_list_loop_back key ls =>
- hash_map_remove_from_list_loop_terminates
- T key ls
+ hash_map_remove_from_list_loop_terminates T key ls
decreasing_by hash_map_remove_from_list_loop_decreases key ls
/- [hashmap::HashMap::{0}::remove_from_list] -/
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] -/