We need to activate autolifting for this:
| (mode autolift) (mode unfold) |
We define lists:
| type 'a list = | Nil | Cons of ('a * 'a list) |
And a map function:
| let rec map f x = match x with | Nil -> Nil | Cons(x,xs) -> Cons(f x, map f xs) |
We want to use vectors of three elements:
| type unit = U type 'a vec3 = Vec3 of 'a * ('a * ('a * unit)) |
They are a specialization of lists:
| type ornament 'a list3 : 'a list => 'a vec3 with | Nil => ~ | Cons(x, xs) => Vec3(x,xs) when xs : 'a list2 and 'a list2 : 'a list => 'a * ('a * unit) with | Nil => ~ | Cons(x,xs) => (x,xs) when xs : 'a list1 and 'a list1 : 'a list => 'a * unit with | Nil => ~ | Cons(x,xs) => (x,xs) when xs : 'a list0 and 'a list0 : 'a list => unit with | Nil => U | Cons(x,xs) => ~ when xs : 'a list0 |
| let map_tuple = lifting map : ('a -> 'b) -> 'a list3 -> 'b list3 |
| let rec map_tuple f x = match x with | Vec3(x, xs) -> Vec3(f x, map_auto1 f xs) and map_auto1 f x = match x with | (x, xs) -> (f x, map_auto2 f xs) and map_auto2 f x = match x with | (x, xs) -> (f x, map_auto3 f xs) and map_auto3 f x = U |