The Factorial Function

First, the usual recursive version:

     dec fact : num -> num;
     --- fact 0 <= 1;
     --- fact n <= n*fact(n-1);

Note that Hope uses best-fit pattern matching, so that the second clause is chosen only if n is non-zero. Moreover, swapping the clauses doesn't change the behaviour of the program.

     fact 7;

Second, a non-recursive version using some libraries:

     uses lists, range;

     dec fact : num -> num;
     --- fact n <= product (1..n);

     1..7;
     product [1, 2, 3, 4, 5, 6, 7];
     fact 7;