|
12196
|
1 |
(* Title : Fact.thy
|
|
|
2 |
Author : Jacques D. Fleuriot
|
|
|
3 |
Copyright : 1998 University of Cambridge
|
|
|
4 |
Description : Factorial function
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
Fact = NatStar +
|
|
|
8 |
|
|
|
9 |
consts fact :: nat => nat
|
|
|
10 |
primrec
|
|
|
11 |
fact_0 "fact 0 = 1"
|
|
|
12 |
fact_Suc "fact (Suc n) = (Suc n) * fact n"
|
|
|
13 |
|
|
|
14 |
end |