fun
fact
(
  n: int
) : int = res where
{
  var n: int = n
  var res: int = 1
  val () = while (n > 0) (res := res * n; n := n - 1)
}