diff options
author | Son Ho | 2024-03-20 06:17:41 +0100 |
---|---|---|
committer | Son Ho | 2024-03-20 06:17:41 +0100 |
commit | 5e99d127e0a746f5779779756fccf79f15c19d10 (patch) | |
tree | 6d10d613179568346e19cbc6bf95c6dd6897f574 /tests/coq/misc/Loops.v | |
parent | e6f002cfc1dfa41362bbb3a005c4261d09c52c58 (diff) |
Regenerate the code
Diffstat (limited to '')
-rw-r--r-- | tests/coq/misc/Loops.v | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index 85b54510..7c83a014 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -29,16 +29,16 @@ Definition sum (n : nat) (max : u32) : result u32 := (** [loops::sum_with_mut_borrows]: loop 0: Source: 'src/loops.rs', lines 19:0-31:1 *) Fixpoint sum_with_mut_borrows_loop - (n : nat) (max : u32) (mi : u32) (ms : u32) : result u32 := + (n : nat) (max : u32) (i : u32) (s : u32) : result u32 := match n with | O => Fail_ OutOfFuel | S n1 => - if mi s< max + if i s< max then ( - ms1 <- u32_add ms mi; - mi1 <- u32_add mi 1%u32; - sum_with_mut_borrows_loop n1 max mi1 ms1) - else u32_mul ms 2%u32 + ms <- u32_add s i; + mi <- u32_add i 1%u32; + sum_with_mut_borrows_loop n1 max mi ms) + else u32_mul s 2%u32 end . @@ -245,10 +245,10 @@ Definition get_elem_mut p <- alloc_vec_Vec_index_mut (List_t usize) usize (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize; - let (l, index_mut_back) := p in - p1 <- get_elem_mut_loop n x l; + let (ls, index_mut_back) := p in + p1 <- get_elem_mut_loop n x ls; let (i, back) := p1 in - let back1 := fun (ret : usize) => l1 <- back ret; index_mut_back l1 in + let back1 := fun (ret : usize) => l <- back ret; index_mut_back l in Return (i, back1) . @@ -273,10 +273,10 @@ Definition get_elem_shared (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) : result usize := - l <- + ls <- alloc_vec_Vec_index (List_t usize) usize (core_slice_index_SliceIndexUsizeSliceTInst (List_t usize)) slots 0%usize; - get_elem_shared_loop n x l + get_elem_shared_loop n x ls . (** [loops::id_mut]: |