summaryrefslogtreecommitdiff
path: root/tests/fstar
diff options
context:
space:
mode:
authorSon Ho2024-01-25 11:54:31 +0100
committerSon Ho2024-01-25 11:54:31 +0100
commitd89cbfdc3f972e1ff4c7c9dd723146556d26526d (patch)
treed948f1104170d7254e8802eb7bf2b77a4386d3b3 /tests/fstar
parentda9a2fb410bde569fea11a4c1507f98ab4250e41 (diff)
Update a decreases clause
Diffstat (limited to '')
-rw-r--r--tests/fstar-split/misc/Loops.Clauses.fst5
1 files changed, 5 insertions, 0 deletions
diff --git a/tests/fstar-split/misc/Loops.Clauses.fst b/tests/fstar-split/misc/Loops.Clauses.fst
index 75194437..13f5513d 100644
--- a/tests/fstar-split/misc/Loops.Clauses.fst
+++ b/tests/fstar-split/misc/Loops.Clauses.fst
@@ -19,6 +19,11 @@ unfold
let sum_with_shared_borrows_loop_decreases (max : u32) (i : u32) (s : u32) : nat =
if max >= i then max - i else 0
+(** [loops::sum_array]: decreases clause *)
+unfold
+let sum_array_loop_decreases (n : usize) (_ : array u32 n) (i : usize) (_ : u32) : nat =
+ if n >= i then n - i else 0
+
(** [loops::clear]: decreases clause *)
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