diff options
Diffstat (limited to 'tests/fstar')
| -rw-r--r-- | tests/fstar/misc/Loops.Funs.fst | 14 |
1 files changed, 3 insertions, 11 deletions
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index d19e9328..c0aca975 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -70,7 +70,7 @@ let sum_with_shared_borrows_fwd (max : u32) : result u32 = sum_with_shared_borrows_loop_fwd max 0 0 (** [loops::clear] *) -let clear_loop_fwd_back +let rec clear_loop_fwd_back (v : vec u32) (i : usize) : Tot (result (vec u32)) (decreases (clear_decreases v i)) = @@ -82,21 +82,13 @@ let clear_loop_fwd_back | Return i1 -> begin match vec_index_mut_back u32 v i 0 with | Fail e -> Fail e - | Return v0 -> - begin match clear_loop_fwd v0 i1 with - | Fail e -> Fail e - | Return _ -> Return v0 - end + | Return v0 -> clear_loop_fwd_back v0 i1 end end else Return v (** [loops::clear] *) -let clear_fwd_back (v : vec u32) : result (vec u32) = - begin match clear_loop_fwd v 0 with - | Fail e -> Fail e - | Return _ -> Return v - end +let clear_fwd_back (v : vec u32) : result (vec u32) = clear_loop_fwd_back v 0 (** [loops::list_mem] *) let rec list_mem_loop_fwd |