Define factorial(n: Integer): Integer by factorial(n) = r | Let r = 1. Let k = 2. While k <= n do Relet r = r * k. Relet k = k + 1. %While %Define