diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/fstar/misc/Loops.Clauses.Template.fst | 105 | ||||
| -rw-r--r-- | tests/fstar/misc/Loops.Funs.fst | 364 |
2 files changed, 453 insertions, 16 deletions
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst index 21c128bb..77f9c3e4 100644 --- a/tests/fstar/misc/Loops.Clauses.Template.fst +++ b/tests/fstar/misc/Loops.Clauses.Template.fst @@ -30,6 +30,111 @@ let sum_array_loop_decreases (n : usize) (a : array u32 n) (i : usize) (s : u32) : nat = admit () +(** [loops::clear]: decreases clause + Source: 'tests/src/loops.rs', lines 62:0-68:1 *) +unfold +let clear_loop_decreases (v : alloc_vec_Vec u32) (i : usize) : nat = admit () + +(** [loops::list_mem]: decreases clause + Source: 'tests/src/loops.rs', lines 76:0-85:1 *) +unfold let list_mem_loop_decreases (x : u32) (ls : list_t u32) : nat = admit () + +(** [loops::list_nth_mut_loop]: decreases clause + Source: 'tests/src/loops.rs', lines 88:0-98:1 *) +unfold +let list_nth_mut_loop_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : + nat = + admit () + +(** [loops::list_nth_shared_loop]: decreases clause + Source: 'tests/src/loops.rs', lines 101:0-111:1 *) +unfold +let list_nth_shared_loop_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : + nat = + admit () + +(** [loops::get_elem_mut]: decreases clause + Source: 'tests/src/loops.rs', lines 113:0-127:1 *) +unfold +let get_elem_mut_loop_decreases (x : usize) (ls : list_t usize) : nat = + admit () + +(** [loops::get_elem_shared]: decreases clause + Source: 'tests/src/loops.rs', lines 129:0-143:1 *) +unfold +let get_elem_shared_loop_decreases (x : usize) (ls : list_t usize) : nat = + admit () + +(** [loops::list_nth_mut_loop_with_id]: decreases clause + Source: 'tests/src/loops.rs', lines 154:0-165:1 *) +unfold +let list_nth_mut_loop_with_id_loop_decreases (t : Type0) (i : u32) + (ls : list_t t) : nat = + admit () + +(** [loops::list_nth_shared_loop_with_id]: decreases clause + Source: 'tests/src/loops.rs', lines 168:0-179:1 *) +unfold +let list_nth_shared_loop_with_id_loop_decreases (t : Type0) (i : u32) + (ls : list_t t) : nat = + admit () + +(** [loops::list_nth_mut_loop_pair]: decreases clause + Source: 'tests/src/loops.rs', lines 184:0-205:1 *) +unfold +let list_nth_mut_loop_pair_loop_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_shared_loop_pair]: decreases clause + Source: 'tests/src/loops.rs', lines 208:0-229:1 *) +unfold +let list_nth_shared_loop_pair_loop_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_mut_loop_pair_merge]: decreases clause + Source: 'tests/src/loops.rs', lines 233:0-248:1 *) +unfold +let list_nth_mut_loop_pair_merge_loop_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_shared_loop_pair_merge]: decreases clause + Source: 'tests/src/loops.rs', lines 251:0-266:1 *) +unfold +let list_nth_shared_loop_pair_merge_loop_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_mut_shared_loop_pair]: decreases clause + Source: 'tests/src/loops.rs', lines 269:0-284:1 *) +unfold +let list_nth_mut_shared_loop_pair_loop_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_mut_shared_loop_pair_merge]: decreases clause + Source: 'tests/src/loops.rs', lines 288:0-303:1 *) +unfold +let list_nth_mut_shared_loop_pair_merge_loop_decreases (t : Type0) + (ls0 : list_t t) (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_shared_mut_loop_pair]: decreases clause + Source: 'tests/src/loops.rs', lines 307:0-322:1 *) +unfold +let list_nth_shared_mut_loop_pair_loop_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_shared_mut_loop_pair_merge]: decreases clause + Source: 'tests/src/loops.rs', lines 326:0-341:1 *) +unfold +let list_nth_shared_mut_loop_pair_merge_loop_decreases (t : Type0) + (ls0 : list_t t) (ls1 : list_t t) (i : u32) : nat = + admit () + (** [loops::ignore_input_mut_borrow]: decreases clause Source: 'tests/src/loops.rs', lines 345:0-349:1 *) unfold let ignore_input_mut_borrow_loop_decreases (i : u32) : nat = admit () diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index dc53a04b..0eafeebb 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -77,15 +77,62 @@ let rec sum_array_loop let sum_array (n : usize) (a : array u32 n) : result u32 = sum_array_loop n a 0 0 +(** [loops::clear]: loop 0: + Source: 'tests/src/loops.rs', lines 62:0-68:1 *) +let rec clear_loop + (v : alloc_vec_Vec u32) (i : usize) : + Tot (result (alloc_vec_Vec u32)) (decreases (clear_loop_decreases v i)) + = + let i1 = alloc_vec_Vec_len u32 v in + if i < i1 + then + let* (_, index_mut_back) = + alloc_vec_Vec_index_mut u32 usize + (core_slice_index_SliceIndexUsizeSliceTInst u32) v i in + let* i2 = usize_add i 1 in + let* v1 = index_mut_back 0 in + clear_loop v1 i2 + else Ok v + (** [loops::clear]: Source: 'tests/src/loops.rs', lines 62:0-62:30 *) let clear (v : alloc_vec_Vec u32) : result (alloc_vec_Vec u32) = - admit + clear_loop v 0 + +(** [loops::list_mem]: loop 0: + Source: 'tests/src/loops.rs', lines 76:0-85:1 *) +let rec list_mem_loop + (x : u32) (ls : list_t u32) : + Tot (result bool) (decreases (list_mem_loop_decreases x ls)) + = + begin match ls with + | List_Cons y tl -> if y = x then Ok true else list_mem_loop x tl + | List_Nil -> Ok false + end (** [loops::list_mem]: Source: 'tests/src/loops.rs', lines 76:0-76:52 *) let list_mem (x : u32) (ls : list_t u32) : result bool = - admit + list_mem_loop x ls + +(** [loops::list_nth_mut_loop]: loop 0: + Source: 'tests/src/loops.rs', lines 88:0-98:1 *) +let rec list_nth_mut_loop_loop + (t : Type0) (ls : list_t t) (i : u32) : + Tot (result (t & (t -> result (list_t t)))) + (decreases (list_nth_mut_loop_loop_decreases t ls i)) + = + begin match ls with + | List_Cons x tl -> + if i = 0 + then let back = fun ret -> Ok (List_Cons ret tl) in Ok (x, back) + else + let* i1 = u32_sub i 1 in + let* (x1, back) = list_nth_mut_loop_loop t tl i1 in + let back1 = fun ret -> let* tl1 = back ret in Ok (List_Cons x tl1) in + Ok (x1, back1) + | List_Nil -> Fail Failure + end (** [loops::list_nth_mut_loop]: Source: 'tests/src/loops.rs', lines 88:0-88:71 *) @@ -93,12 +140,44 @@ let list_nth_mut_loop (t : Type0) (ls : list_t t) (i : u32) : result (t & (t -> result (list_t t))) = - admit + list_nth_mut_loop_loop t ls i + +(** [loops::list_nth_shared_loop]: loop 0: + Source: 'tests/src/loops.rs', lines 101:0-111:1 *) +let rec list_nth_shared_loop_loop + (t : Type0) (ls : list_t t) (i : u32) : + Tot (result t) (decreases (list_nth_shared_loop_loop_decreases t ls i)) + = + begin match ls with + | List_Cons x tl -> + if i = 0 + then Ok x + else let* i1 = u32_sub i 1 in list_nth_shared_loop_loop t tl i1 + | List_Nil -> Fail Failure + end (** [loops::list_nth_shared_loop]: Source: 'tests/src/loops.rs', lines 101:0-101:66 *) let list_nth_shared_loop (t : Type0) (ls : list_t t) (i : u32) : result t = - admit + list_nth_shared_loop_loop t ls i + +(** [loops::get_elem_mut]: loop 0: + Source: 'tests/src/loops.rs', lines 113:0-127:1 *) +let rec get_elem_mut_loop + (x : usize) (ls : list_t usize) : + Tot (result (usize & (usize -> result (list_t usize)))) + (decreases (get_elem_mut_loop_decreases x ls)) + = + begin match ls with + | List_Cons y tl -> + if y = x + then let back = fun ret -> Ok (List_Cons ret tl) in Ok (y, back) + else + let* (i, back) = get_elem_mut_loop x tl in + let back1 = fun ret -> let* tl1 = back ret in Ok (List_Cons y tl1) in + Ok (i, back1) + | List_Nil -> Fail Failure + end (** [loops::get_elem_mut]: Source: 'tests/src/loops.rs', lines 113:0-113:73 *) @@ -106,13 +185,32 @@ let get_elem_mut (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result (usize & (usize -> result (alloc_vec_Vec (list_t usize)))) = - admit + let* (ls, index_mut_back) = + alloc_vec_Vec_index_mut (list_t usize) usize + (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in + let* (i, back) = get_elem_mut_loop x ls in + let back1 = fun ret -> let* l = back ret in index_mut_back l in + Ok (i, back1) + +(** [loops::get_elem_shared]: loop 0: + Source: 'tests/src/loops.rs', lines 129:0-143:1 *) +let rec get_elem_shared_loop + (x : usize) (ls : list_t usize) : + Tot (result usize) (decreases (get_elem_shared_loop_decreases x ls)) + = + begin match ls with + | List_Cons y tl -> if y = x then Ok y else get_elem_shared_loop x tl + | List_Nil -> Fail Failure + end (** [loops::get_elem_shared]: Source: 'tests/src/loops.rs', lines 129:0-129:68 *) let get_elem_shared (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize = - admit + let* ls = + alloc_vec_Vec_index (list_t usize) usize + (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in + get_elem_shared_loop x ls (** [loops::id_mut]: Source: 'tests/src/loops.rs', lines 145:0-145:50 *) @@ -127,19 +225,85 @@ let id_mut let id_shared (t : Type0) (ls : list_t t) : result (list_t t) = Ok ls +(** [loops::list_nth_mut_loop_with_id]: loop 0: + Source: 'tests/src/loops.rs', lines 154:0-165:1 *) +let rec list_nth_mut_loop_with_id_loop + (t : Type0) (i : u32) (ls : list_t t) : + Tot (result (t & (t -> result (list_t t)))) + (decreases (list_nth_mut_loop_with_id_loop_decreases t i ls)) + = + begin match ls with + | List_Cons x tl -> + if i = 0 + then let back = fun ret -> Ok (List_Cons ret tl) in Ok (x, back) + else + let* i1 = u32_sub i 1 in + let* (x1, back) = list_nth_mut_loop_with_id_loop t i1 tl in + let back1 = fun ret -> let* tl1 = back ret in Ok (List_Cons x tl1) in + Ok (x1, back1) + | List_Nil -> Fail Failure + end + (** [loops::list_nth_mut_loop_with_id]: Source: 'tests/src/loops.rs', lines 154:0-154:75 *) let list_nth_mut_loop_with_id (t : Type0) (ls : list_t t) (i : u32) : result (t & (t -> result (list_t t))) = - admit + let* (ls1, id_mut_back) = id_mut t ls in + let* (x, back) = list_nth_mut_loop_with_id_loop t i ls1 in + let back1 = fun ret -> let* l = back ret in id_mut_back l in + Ok (x, back1) + +(** [loops::list_nth_shared_loop_with_id]: loop 0: + Source: 'tests/src/loops.rs', lines 168:0-179:1 *) +let rec list_nth_shared_loop_with_id_loop + (t : Type0) (i : u32) (ls : list_t t) : + Tot (result t) + (decreases (list_nth_shared_loop_with_id_loop_decreases t i ls)) + = + begin match ls with + | List_Cons x tl -> + if i = 0 + then Ok x + else let* i1 = u32_sub i 1 in list_nth_shared_loop_with_id_loop t i1 tl + | List_Nil -> Fail Failure + end (** [loops::list_nth_shared_loop_with_id]: Source: 'tests/src/loops.rs', lines 168:0-168:70 *) let list_nth_shared_loop_with_id (t : Type0) (ls : list_t t) (i : u32) : result t = - admit + let* ls1 = id_shared t ls in list_nth_shared_loop_with_id_loop t i ls1 + +(** [loops::list_nth_mut_loop_pair]: loop 0: + Source: 'tests/src/loops.rs', lines 184:0-205:1 *) +let rec list_nth_mut_loop_pair_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result ((t & t) & (t -> result (list_t t)) & (t -> result (list_t t)))) + (decreases (list_nth_mut_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then + let back'a = fun ret -> Ok (List_Cons ret tl0) in + let back'b = fun ret -> Ok (List_Cons ret tl1) in + Ok ((x0, x1), back'a, back'b) + else + let* i1 = u32_sub i 1 in + let* (p, back'a, back'b) = list_nth_mut_loop_pair_loop t tl0 tl1 i1 in + let back'a1 = + fun ret -> let* tl01 = back'a ret in Ok (List_Cons x0 tl01) in + let back'b1 = + fun ret -> let* tl11 = back'b ret in Ok (List_Cons x1 tl11) in + Ok (p, back'a1, back'b1) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end (** [loops::list_nth_mut_loop_pair]: Source: 'tests/src/loops.rs', lines 184:0-188:27 *) @@ -147,13 +311,62 @@ let list_nth_mut_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t)) & (t -> result (list_t t))) = - admit + list_nth_mut_loop_pair_loop t ls0 ls1 i + +(** [loops::list_nth_shared_loop_pair]: loop 0: + Source: 'tests/src/loops.rs', lines 208:0-229:1 *) +let rec list_nth_shared_loop_pair_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_shared_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Ok (x0, x1) + else let* i1 = u32_sub i 1 in list_nth_shared_loop_pair_loop t tl0 tl1 i1 + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end (** [loops::list_nth_shared_loop_pair]: Source: 'tests/src/loops.rs', lines 208:0-212:19 *) let list_nth_shared_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = - admit + list_nth_shared_loop_pair_loop t ls0 ls1 i + +(** [loops::list_nth_mut_loop_pair_merge]: loop 0: + Source: 'tests/src/loops.rs', lines 233:0-248:1 *) +let rec list_nth_mut_loop_pair_merge_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result ((t & t) & ((t & t) -> result ((list_t t) & (list_t t))))) + (decreases (list_nth_mut_loop_pair_merge_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then + let back = + fun ret -> + let (x, x2) = ret in Ok (List_Cons x tl0, List_Cons x2 tl1) in + Ok ((x0, x1), back) + else + let* i1 = u32_sub i 1 in + let* (p, back) = list_nth_mut_loop_pair_merge_loop t tl0 tl1 i1 in + let back1 = + fun ret -> + let* (tl01, tl11) = back ret in + Ok (List_Cons x0 tl01, List_Cons x1 tl11) in + Ok (p, back1) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end (** [loops::list_nth_mut_loop_pair_merge]: Source: 'tests/src/loops.rs', lines 233:0-237:27 *) @@ -161,13 +374,58 @@ let list_nth_mut_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & ((t & t) -> result ((list_t t) & (list_t t)))) = - admit + list_nth_mut_loop_pair_merge_loop t ls0 ls1 i + +(** [loops::list_nth_shared_loop_pair_merge]: loop 0: + Source: 'tests/src/loops.rs', lines 251:0-266:1 *) +let rec list_nth_shared_loop_pair_merge_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_shared_loop_pair_merge_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Ok (x0, x1) + else + let* i1 = u32_sub i 1 in + list_nth_shared_loop_pair_merge_loop t tl0 tl1 i1 + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end (** [loops::list_nth_shared_loop_pair_merge]: Source: 'tests/src/loops.rs', lines 251:0-255:19 *) let list_nth_shared_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = - admit + list_nth_shared_loop_pair_merge_loop t ls0 ls1 i + +(** [loops::list_nth_mut_shared_loop_pair]: loop 0: + Source: 'tests/src/loops.rs', lines 269:0-284:1 *) +let rec list_nth_mut_shared_loop_pair_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result ((t & t) & (t -> result (list_t t)))) + (decreases (list_nth_mut_shared_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then let back = fun ret -> Ok (List_Cons ret tl0) in Ok ((x0, x1), back) + else + let* i1 = u32_sub i 1 in + let* (p, back) = list_nth_mut_shared_loop_pair_loop t tl0 tl1 i1 in + let back1 = fun ret -> let* tl01 = back ret in Ok (List_Cons x0 tl01) + in + Ok (p, back1) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end (** [loops::list_nth_mut_shared_loop_pair]: Source: 'tests/src/loops.rs', lines 269:0-273:23 *) @@ -175,7 +433,32 @@ let list_nth_mut_shared_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t))) = - admit + list_nth_mut_shared_loop_pair_loop t ls0 ls1 i + +(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: + Source: 'tests/src/loops.rs', lines 288:0-303:1 *) +let rec list_nth_mut_shared_loop_pair_merge_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result ((t & t) & (t -> result (list_t t)))) + (decreases (list_nth_mut_shared_loop_pair_merge_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then let back = fun ret -> Ok (List_Cons ret tl0) in Ok ((x0, x1), back) + else + let* i1 = u32_sub i 1 in + let* (p, back) = list_nth_mut_shared_loop_pair_merge_loop t tl0 tl1 i1 + in + let back1 = fun ret -> let* tl01 = back ret in Ok (List_Cons x0 tl01) + in + Ok (p, back1) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end (** [loops::list_nth_mut_shared_loop_pair_merge]: Source: 'tests/src/loops.rs', lines 288:0-292:23 *) @@ -183,7 +466,31 @@ let list_nth_mut_shared_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t))) = - admit + list_nth_mut_shared_loop_pair_merge_loop t ls0 ls1 i + +(** [loops::list_nth_shared_mut_loop_pair]: loop 0: + Source: 'tests/src/loops.rs', lines 307:0-322:1 *) +let rec list_nth_shared_mut_loop_pair_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result ((t & t) & (t -> result (list_t t)))) + (decreases (list_nth_shared_mut_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then let back = fun ret -> Ok (List_Cons ret tl1) in Ok ((x0, x1), back) + else + let* i1 = u32_sub i 1 in + let* (p, back) = list_nth_shared_mut_loop_pair_loop t tl0 tl1 i1 in + let back1 = fun ret -> let* tl11 = back ret in Ok (List_Cons x1 tl11) + in + Ok (p, back1) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end (** [loops::list_nth_shared_mut_loop_pair]: Source: 'tests/src/loops.rs', lines 307:0-311:23 *) @@ -191,7 +498,32 @@ let list_nth_shared_mut_loop_pair (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t))) = - admit + list_nth_shared_mut_loop_pair_loop t ls0 ls1 i + +(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: + Source: 'tests/src/loops.rs', lines 326:0-341:1 *) +let rec list_nth_shared_mut_loop_pair_merge_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result ((t & t) & (t -> result (list_t t)))) + (decreases (list_nth_shared_mut_loop_pair_merge_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then let back = fun ret -> Ok (List_Cons ret tl1) in Ok ((x0, x1), back) + else + let* i1 = u32_sub i 1 in + let* (p, back) = list_nth_shared_mut_loop_pair_merge_loop t tl0 tl1 i1 + in + let back1 = fun ret -> let* tl11 = back ret in Ok (List_Cons x1 tl11) + in + Ok (p, back1) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end (** [loops::list_nth_shared_mut_loop_pair_merge]: Source: 'tests/src/loops.rs', lines 326:0-330:23 *) @@ -199,7 +531,7 @@ let list_nth_shared_mut_loop_pair_merge (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result ((t & t) & (t -> result (list_t t))) = - admit + list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i (** [loops::ignore_input_mut_borrow]: loop 0: Source: 'tests/src/loops.rs', lines 345:0-349:1 *) |