summaryrefslogtreecommitdiff
path: root/tests/coq/misc
diff options
context:
space:
mode:
Diffstat (limited to 'tests/coq/misc')
-rw-r--r--tests/coq/misc/Loops.v64
1 files changed, 64 insertions, 0 deletions
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 8260db02..e235b60d 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -688,4 +688,68 @@ Definition list_nth_shared_mut_loop_pair_merge
Return (p1, back_'a)
.
+(** [loops::ignore_input_mut_borrow]: loop 0:
+ Source: 'src/loops.rs', lines 345:0-349:1 *)
+Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n1 =>
+ if i s> 0%u32
+ then (
+ i1 <- u32_sub i 1%u32; _ <- ignore_input_mut_borrow_loop n1 i1; Return tt)
+ else Return tt
+ end
+.
+
+(** [loops::ignore_input_mut_borrow]:
+ Source: 'src/loops.rs', lines 345:0-345:56 *)
+Definition ignore_input_mut_borrow
+ (n : nat) (_a : u32) (i : u32) : result u32 :=
+ _ <- ignore_input_mut_borrow_loop n i; Return _a
+.
+
+(** [loops::incr_ignore_input_mut_borrow]: loop 0:
+ Source: 'src/loops.rs', lines 353:0-358:1 *)
+Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n1 =>
+ if i s> 0%u32
+ then (
+ i1 <- u32_sub i 1%u32;
+ _ <- incr_ignore_input_mut_borrow_loop n1 i1;
+ Return tt)
+ else Return tt
+ end
+.
+
+(** [loops::incr_ignore_input_mut_borrow]:
+ Source: 'src/loops.rs', lines 353:0-353:60 *)
+Definition incr_ignore_input_mut_borrow
+ (n : nat) (a : u32) (i : u32) : result u32 :=
+ a1 <- u32_add a 1%u32; _ <- incr_ignore_input_mut_borrow_loop n i; Return a1
+.
+
+(** [loops::ignore_input_shared_borrow]: loop 0:
+ Source: 'src/loops.rs', lines 362:0-366:1 *)
+Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n1 =>
+ if i s> 0%u32
+ then (
+ i1 <- u32_sub i 1%u32;
+ _ <- ignore_input_shared_borrow_loop n1 i1;
+ Return tt)
+ else Return tt
+ end
+.
+
+(** [loops::ignore_input_shared_borrow]:
+ Source: 'src/loops.rs', lines 362:0-362:59 *)
+Definition ignore_input_shared_borrow
+ (n : nat) (_a : u32) (i : u32) : result u32 :=
+ _ <- ignore_input_shared_borrow_loop n i; Return _a
+.
+
End Loops.