5 lines
98 B
Text
5 lines
98 B
Text
|
def factorial (n : Nat) : Nat :=
|
||
|
|
match n with
|
||
|
|
| 0 => 1
|
||
|
|
| (k + 1) => (k + 1) * factorial (k)
|