diff options
| author | Son Ho | 2023-01-13 16:44:25 +0100 |
|---|---|---|
| committer | Son HO | 2023-02-03 11:21:46 +0100 |
| commit | c52add165764d3a0b68ee5181901109078e9b19b (patch) | |
| tree | 782758a96e6b1a8b9998e631a2a91af193846459 /tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst | |
| parent | e69382acbcc4bdd27612c9cf8ec282db71f8408d (diff) | |
Update the hashmap and regenerate
Diffstat (limited to 'tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst')
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst index f3afa008..1e15d1f9 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst @@ -12,9 +12,9 @@ let hashmap_hash_map_allocate_slots_loop_decreases (t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) : nat = admit () -(** [hashmap_main::hashmap::HashMap::{0}::clear_slots]: decreases clause *) +(** [hashmap_main::hashmap::HashMap::{0}::clear]: decreases clause *) unfold -let hashmap_hash_map_clear_slots_loop_decreases (t : Type0) +let hashmap_hash_map_clear_loop_decreases (t : Type0) (slots : vec (hashmap_list_t t)) (i : usize) : nat = admit () |