datatype Expr where
| Var(Int)
| Abs(Int, Expr)
| App(Expr, Expr)
end
datatype List[a] where
| Nil
| Cons(a, List[a])
end
function remove(xs: List[Int], x: Int) -> List[Int]
begin
match xs with
| Nil => Nil
| Cons(head, tail) =>
if head == x then remove(tail, x)
else Cons(head, remove(tail, x))
end
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 free_vars(expr: Expr) -> List[Int]
begin
match expr with
| Var(x) => Cons(x, Nil)
| Abs(x, e) => remove(free_vars(e), x)
| App(e1, e2) =>
let v1 = free_vars(e1);
let v2 = free_vars(e2);
concat(v1, v2)
end
end
function example(expr: Expr)
begin
guard free_vars(expr) = Nil;
end
query example(depth_step=5, depth_limit=30, answer_limit=100)