Regenerate test output

1 files changed, 23 insertions, 1 deletions

diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index c78dab8e..41fd9804 100644
--- a/tests/fstar/demo/Demo.fst
+++ b/tests/fstar/demo/Demo.fst
@@ -76,13 +76,35 @@ let rec list_nth_mut
     | CList_CNil -> Fail Failure
     end
 
+(** [demo::list_nth_mut1]: loop 0:
+    Source: 'tests/src/demo.rs', lines 69:0-78:1 *)
+let rec list_nth_mut1_loop
+  (t : Type0) (n : nat) (l : cList_t t) (i : u32) :
+  result (t & (t -> result (cList_t t)))
+  =
+  if is_zero n
+  then Fail OutOfFuel
+  else
+    let n1 = decrease n in
+    begin match l with
+    | CList_CCons x tl ->
+      if i = 0
+      then let back = fun ret -> Ok (CList_CCons ret tl) in Ok (x, back)
+      else
+        let* i1 = u32_sub i 1 in
+        let* (x1, back) = list_nth_mut1_loop t n1 tl i1 in
+        let back1 = fun ret -> let* tl1 = back ret in Ok (CList_CCons x tl1) in
+        Ok (x1, back1)
+    | CList_CNil -> Fail Failure
+    end
+
 (** [demo::list_nth_mut1]:
     Source: 'tests/src/demo.rs', lines 69:0-69:77 *)
 let list_nth_mut1
   (t : Type0) (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]:
     Source: 'tests/src/demo.rs', lines 80:0-80:28 *)