1 files changed, 26 insertions, 1 deletions
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index 14b1ca9d..8d8f840d 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -90,13 +90,38 @@ Fixpoint list_nth_mut
   end
 .
 
+(** [demo::list_nth_mut1]: loop 0:
+    Source: 'tests/src/demo.rs', lines 69:0-78:1 *)
+Fixpoint list_nth_mut1_loop
+  (T : Type) (n : nat) (l : CList_t T) (i : u32) :
+  result (T * (T -> result (CList_t T)))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    match l with
+    | CList_CCons x tl =>
+      if i s= 0%u32
+      then let back := fun (ret : T) => Ok (CList_CCons ret tl) in Ok (x, back)
+      else (
+        i1 <- u32_sub i 1%u32;
+        p <- list_nth_mut1_loop T n1 tl i1;
+        let (t, back) := p in
+        let back1 := fun (ret : T) => tl1 <- back ret; Ok (CList_CCons x tl1)
+          in
+        Ok (t, back1))
+    | CList_CNil => Fail_ Failure
+    end
+  end
+.
+
 (** [demo::list_nth_mut1]:
     Source: 'tests/src/demo.rs', lines 69:0-69:77 *)
 Definition list_nth_mut1
   (T : Type) (n : nat) (l : CList_t T) (i : u32) :
   result (T * (T -> result (CList_t T)))
   :=
-  admit
+  list_nth_mut1_loop T n l i
 .
 
 (** [demo::i32_id]: