summaryrefslogtreecommitdiff
path: root/tests/fstar/misc/Loops.Clauses.fst
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar/misc/Loops.Clauses.fst')
-rw-r--r--tests/fstar/misc/Loops.Clauses.fst51
1 files changed, 48 insertions, 3 deletions
diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst
index d315a4f0..9cf5db1f 100644
--- a/tests/fstar/misc/Loops.Clauses.fst
+++ b/tests/fstar/misc/Loops.Clauses.fst
@@ -9,25 +9,70 @@ open Loops.Types
unfold let sum_decreases (max : u32) (i : u32) (s : u32) : nat =
if i <= max then max - i else 0
+(** [loops::sum_with_mut_borrows]: decreases clause *)
+unfold
+let sum_with_mut_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
+ if max >= mi then max - mi else 0
-(** [loops::sum_with_borrows]: decreases clause *)
+(** [loops::sum_with_shared_borrows]: decreases clause *)
unfold
-let sum_with_borrows_decreases (max : u32) (mi : u32) (ms : u32) : nat =
- if mi <= max then max - mi else 0
+let sum_with_shared_borrows_decreases (max : u32) (i : u32) (s : u32) : nat =
+ if max >= i then max - i else 0
(** [loops::list_nth_mut_loop]: decreases clause *)
unfold
let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat =
i
+(** [loops::list_nth_shared_loop]: decreases clause *)
+unfold
+let list_nth_shared_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : list_t t =
+ ls
+
(** [loops::list_nth_mut_loop_pair]: decreases clause *)
unfold
let list_nth_mut_loop_pair_decreases (t : Type0) (l : list_t t) (l0 : list_t t)
(i : u32) : nat =
i
+(** [loops::list_nth_shared_loop_pair]: decreases clause *)
+unfold
+let list_nth_shared_loop_pair_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : list_t t =
+ l
+
(** [loops::list_nth_mut_loop_pair_merge]: decreases clause *)
unfold
let list_nth_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t)
(l0 : list_t t) (i : u32) : nat =
i
+
+(** [loops::list_nth_shared_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : list_t t =
+ l
+
+(** [loops::list_nth_mut_shared_loop_pair]: decreases clause *)
+unfold
+let list_nth_mut_shared_loop_pair_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : list_t t =
+ l
+
+(** [loops::list_nth_mut_shared_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_mut_shared_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : list_t t =
+ l
+
+(** [loops::list_nth_shared_mut_loop_pair]: decreases clause *)
+unfold
+let list_nth_shared_mut_loop_pair_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : list_t t =
+ l
+
+(** [loops::list_nth_shared_mut_loop_pair_merge]: decreases clause *)
+unfold
+let list_nth_shared_mut_loop_pair_merge_decreases (t : Type0) (l : list_t t)
+ (l0 : list_t t) (i : u32) : list_t t =
+ l