diff options
Diffstat (limited to 'tests/coq/misc/Loops.v')
| -rw-r--r-- | tests/coq/misc/Loops.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index bcbfc8df..a5cb3688 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -19,7 +19,7 @@ Fixpoint sum_loop_fwd (n : nat) (max : u32) (i : u32) (s : u32) : result u32 := (** [loops::sum] *) Definition sum_fwd (n : nat) (max : u32) : result u32 := - sum_loop_fwd n max (0%u32) (0%u32) + sum_loop_fwd n max 0%u32 0%u32 . (** [loops::sum_with_mut_borrows] *) @@ -39,7 +39,7 @@ Fixpoint sum_with_mut_borrows_loop_fwd (** [loops::sum_with_mut_borrows] *) Definition sum_with_mut_borrows_fwd (n : nat) (max : u32) : result u32 := - sum_with_mut_borrows_loop_fwd n max (0%u32) (0%u32) + sum_with_mut_borrows_loop_fwd n max 0%u32 0%u32 . (** [loops::sum_with_shared_borrows] *) @@ -59,7 +59,7 @@ Fixpoint sum_with_shared_borrows_loop_fwd (** [loops::sum_with_shared_borrows] *) Definition sum_with_shared_borrows_fwd (n : nat) (max : u32) : result u32 := - sum_with_shared_borrows_loop_fwd n max (0%u32) (0%u32) + sum_with_shared_borrows_loop_fwd n max 0%u32 0%u32 . (** [loops::clear] *) @@ -72,7 +72,7 @@ Fixpoint clear_loop_fwd_back if i s< i0 then ( i1 <- usize_add i 1%usize; - v0 <- vec_index_mut_back u32 v i (0%u32); + v0 <- vec_index_mut_back u32 v i 0%u32; clear_loop_fwd_back n0 v0 i1) else Return v end @@ -80,7 +80,7 @@ Fixpoint clear_loop_fwd_back (** [loops::clear] *) Definition clear_fwd_back (n : nat) (v : vec u32) : result (vec u32) := - clear_loop_fwd_back n v (0%usize) + clear_loop_fwd_back n v 0%usize . (** [loops::List] *) @@ -201,7 +201,7 @@ Fixpoint get_elem_mut_loop_fwd (** [loops::get_elem_mut] *) Definition get_elem_mut_fwd (n : nat) (slots : vec (List_t usize)) (x : usize) : result usize := - l <- vec_index_mut_fwd (List_t usize) slots (0%usize); + l <- vec_index_mut_fwd (List_t usize) slots 0%usize; get_elem_mut_loop_fwd n x l . @@ -228,9 +228,9 @@ Definition get_elem_mut_back (n : nat) (slots : vec (List_t usize)) (x : usize) (ret : usize) : result (vec (List_t usize)) := - l <- vec_index_mut_fwd (List_t usize) slots (0%usize); + l <- vec_index_mut_fwd (List_t usize) slots 0%usize; l0 <- get_elem_mut_loop_back n x l ret; - vec_index_mut_back (List_t usize) slots (0%usize) l0 + vec_index_mut_back (List_t usize) slots 0%usize l0 . (** [loops::get_elem_shared] *) @@ -250,7 +250,7 @@ Fixpoint get_elem_shared_loop_fwd (** [loops::get_elem_shared] *) Definition get_elem_shared_fwd (n : nat) (slots : vec (List_t usize)) (x : usize) : result usize := - l <- vec_index_fwd (List_t usize) slots (0%usize); + l <- vec_index_fwd (List_t usize) slots 0%usize; get_elem_shared_loop_fwd n x l . |