diff options
| author | Son Ho | 2023-12-05 17:34:13 +0100 |
|---|---|---|
| committer | Son Ho | 2023-12-05 17:34:13 +0100 |
| commit | 726db4911add81a853aafcec3936b457aaeff5b4 (patch) | |
| tree | 2663915767c3558203990ed14f8d5604b7fd21d1 /tests/fstar/misc/Loops.Clauses.fst | |
| parent | 92887b89e35607e99bae2f19e4c5b2f162683d02 (diff) | |
| parent | 4795e5f823bc89504855d8eb946b111d9314f4d5 (diff) | |
Merge branch 'main' into son_fixes2
Diffstat (limited to 'tests/fstar/misc/Loops.Clauses.fst')
| -rw-r--r-- | tests/fstar/misc/Loops.Clauses.fst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst index 82f34de1..75194437 100644 --- a/tests/fstar/misc/Loops.Clauses.fst +++ b/tests/fstar/misc/Loops.Clauses.fst @@ -20,7 +20,7 @@ let sum_with_shared_borrows_loop_decreases (max : u32) (i : u32) (s : u32) : nat if max >= i then max - i else 0 (** [loops::clear]: decreases clause *) -unfold let clear_loop_decreases (v : vec u32) (i : usize) : nat = +unfold let clear_loop_decreases (v : alloc_vec_Vec u32) (i : usize) : nat = if i <= List.Tot.length v then List.Tot.length v - i else 0 (** [loops::list_mem]: decreases clause *) |