diff options
Diffstat (limited to '')
| -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 *) |