Commit

// A number is prime when it is at least 2 and nothing from 2 up to it divides it.
fn is_prime(n: Int) -> Bool
  ensures result == ((n >= 2) and (forall k in 2..n: (n % k) != 0))
do
  if n < 2 then
    return false
  end if
  var d = 2
  while d < n
    invariant (2 <= d) and (d <= n)
    invariant forall k in 2..d: (n % k) != 0
    decreases n - d
  do
    if (n % d) == 0 then
      return false
    end if
    set d = d + 1
  end while
  return true
end fn is_prime