datatype List[a] where
| Nil
| Cons(a, List[a])
end
function reverse[a](xs: List[a]) -> List[a]
begin
reverse_help(xs, Nil)
end
function reverse_help[a](xs: List[a], ys: List[a]) -> List[a]
begin
match xs with
| Nil => ys
| Cons(head, tail) => reverse_help(tail, Cons(head, 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(ys: List[Int])
begin
guard ys = reverse(rev_nat_list(100));
end
query example(depth_step=50, depth_limit=1000, answer_limit=1)