diff options
author | Son Ho | 2023-01-06 01:10:51 +0100 |
---|---|---|
committer | Son HO | 2023-02-03 11:21:46 +0100 |
commit | a2e52dd8e4f53600c74744026aeae15d99d104b0 (patch) | |
tree | ad5c81fd1e9763955d1c8250d3dc730f39f678d5 /tests/fstar | |
parent | 852ee63cb876d419d4830eb5192604d58b07b495 (diff) |
Fix an issue with the translation of loops::clear
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 |