Demo Dependent Types

extern fun is_equal {m,n:int} (int m, int n): bool (m==n)
implement is_equal {m,n} (x, y) = (x <= y+1) * (x >= y-1)