summaryrefslogtreecommitdiff
path: root/tests/fstar/misc/Loops.Clauses.fst
diff options
context:
space:
mode:
authorSon Ho2023-11-29 14:26:04 +0100
committerSon Ho2023-11-29 14:26:04 +0100
commit0273fee7f6b74da1d3b66c3c6a2158c012d04197 (patch)
tree5f6db32814f6f0b3a98f2de1db39225ff2c7645d /tests/fstar/misc/Loops.Clauses.fst
parentf4e2c2bb09d9d7b54afc0692b7f690f5ec2eb029 (diff)
parent90e42e0e1c1889aabfa66283fb15b43a5852a02a (diff)
Merge branch 'main' into afromher_shifts
Diffstat (limited to '')
-rw-r--r--tests/fstar/misc/Loops.Clauses.fst2
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 *)