THEORY factorial
BEGIN
n: VAR nat
factorial(n): RECURSIVE posnat =
(IF n = 0 THEN 1 ELSE n * factorial(n-1) ENDIF)
MEASURE n
END factorial