datatype List[a] where
| Nil
| Cons(a, List[a])
end
function concat[a](xs: List[a], ys: List[a]) -> List[a]
begin
match xs with
| Nil => ys
| Cons(head, tail) => Cons(head, concat(tail, ys))
end
end
function rev_nat_list(n: Int) -> List[Int]
begin
if n == 0 then Nil
else Cons(n, rev_nat_list(n - 1))
end
function example(xs: List[Int], ys: List[Int])
begin
guard concat(xs, ys) = rev_nat_list(100);
end
query example(depth_step=50, depth_limit=1000, answer_limit=101)