\func
fac
(
n
:
Nat
)
:
Nat
|
0
=>
1
|
suc
n
=>
suc
n
Nat
.
*
fac
n