/*
{n:nat}
int fact (x: int(n)) {
  var: int y;;
  y = 1;

  invariant: [i:nat] (x: int(i))
  while (x > 0) {
    y = y * x; x = x - 1;
  }

  return y;
}
*/

{n:nat}
int fact (x: int(n)) {
  var: int y;;
  if (x > 0) { y = fact (x-1); return x * y; } else return 1;
}

int main () {
  var: int x;;
  x = 10;
  return fact (x);
}