(*
 * This simple example says that reversing a
 * list yields a list of the same length.
 *)

fun('a) reverse(l) =
let
    fun aux(nil, ys) = ys
      | aux(x::xs, ys) = aux(xs, x::ys)
    where aux <| {m:nat,n:nat} 'a list(m) * 'a list(n) -> 'a list(m+n)
in
    aux(l, [])
end
where reverse <| {n:nat} 'a list(n) -> 'a list(n)