1 files changed, 24 insertions, 1 deletions
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 7402f010..a9b349b3 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -87,13 +87,36 @@ divergent def list_nth_mut
       Result.ok (t, back)
   | CList.CNil => Result.fail .panic
 
+/- [demo::list_nth_mut1]: loop 0:
+   Source: 'tests/src/demo.rs', lines 69:0-78:1 -/
+divergent def list_nth_mut1_loop
+  (T : Type) (l : CList T) (i : U32) :
+  Result (T × (T → Result (CList T)))
+  :=
+  match l with
+  | CList.CCons x tl =>
+    if i = 0#u32
+    then
+      let back := fun ret => Result.ok (CList.CCons ret tl)
+      Result.ok (x, back)
+    else
+      do
+      let i1 ← i - 1#u32
+      let (t, back) ← list_nth_mut1_loop T tl i1
+      let back1 :=
+        fun ret => do
+                   let tl1 ← back ret
+                   Result.ok (CList.CCons x tl1)
+      Result.ok (t, back1)
+  | CList.CNil => Result.fail .panic
+
 /- [demo::list_nth_mut1]:
    Source: 'tests/src/demo.rs', lines 69:0-69:77 -/
 def list_nth_mut1
   (T : Type) (l : CList T) (i : U32) :
   Result (T × (T → Result (CList T)))
   :=
-  sorry
+  list_nth_mut1_loop T l i
 
 /- [demo::i32_id]:
    Source: 'tests/src/demo.rs', lines 80:0-80:28 -/