7 lines
170 B
Agda
7 lines
170 B
Agda
module Factorial where
|
||
|
||
open import Data.Nat using (ℕ ; zero ; suc ; _*_)
|
||
|
||
factorial : (n : ℕ) → ℕ
|
||
factorial zero = 1
|
||
factorial (suc n) = (suc n) * (factorial n)
|