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