diff options
| author | Son Ho | 2023-10-27 12:26:20 +0200 |
|---|---|---|
| committer | Son Ho | 2023-10-27 12:26:20 +0200 |
| commit | 67fb76ae5801fdb8f134394425e466dbe611a54b (patch) | |
| tree | 943235f1771e36fea607636dc09d25c21dab30e8 /tests/fstar/hashmap_on_disk/Primitives.fst | |
| parent | 1c4b1222dbf5e090c26e613694d63577343ab2fd (diff) | |
Regenerate more F* files
Diffstat (limited to 'tests/fstar/hashmap_on_disk/Primitives.fst')
| -rw-r--r-- | tests/fstar/hashmap_on_disk/Primitives.fst | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst index 3110b247..71d75c11 100644 --- a/tests/fstar/hashmap_on_disk/Primitives.fst +++ b/tests/fstar/hashmap_on_disk/Primitives.fst @@ -707,5 +707,7 @@ let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0) let alloc_vec_Vec_index_mut_back_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : Lemma ( alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x == - alloc_vec_Vec_update_usize v i x) = + alloc_vec_Vec_update_usize v i x) + [SMTPat (alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x)] + = admit() |