``` 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75``` ```open list val convert (): () = () alias convertible (p: perm) (q: perm): perm = convert @ (| consumes p) -> (| q) data mutable iterator a (hole: perm) (post: perm) = Iterator { content: {p: perm} ( l: list a | p * convertible (p * hole * l @ list a) post ) } data offer a (post: perm) = | None { | post } | Some { x: a } val next [a, hole: perm, post: perm] (consumes (it: iterator a hole post | hole)): offer (x: a | it @ iterator a (x @ a) post) post = match it.content with | Nil -> convert (); None | Cons { head; tail } -> it.content <- tail; Some { x = head } end val stop [a, hole: perm, post: perm] (consumes (it: iterator a hole post | hole)): (| post) = convert () val new [a] (consumes l: list a): iterator a empty (l @ list a) = Iterator { content = l } (* -------------------------------------------- *) val rec loop [a, hole: perm, post: perm] (consumes (it: iterator a hole post | hole), f: a -> ()): (| post) = match next [hole = hole] it with | None -> assert post; () | Some { x } -> f x; loop [hole = (x @ a)] (it, f) end val rec nth [a, hole: perm, post: perm] (consumes it: (iterator a hole post | hole), n: int): offer (x: a | it @ iterator a (x @ a) post) post = match next [hole = hole] it with | None -> None | Some { x } -> if n <= 0 then ( Some { x = x } ) else ( nth [a = a, hole = (x @ a)] (it, n-1) ) end val _ = let l = three (1, 2, 3) in let it = new l in match nth [hole = empty] (it, 1) with | None -> () | Some { x } -> (* Do stuff on x *) print x; (* Give (x @ int) back to the list, close the iteration *) stop it end (* l @ list int *) ```