Factorial: Difference between revisions
→{{header|Agda}}: Updated Agda example
(→{{header|Coq}}: Added Coq example) |
(→{{header|Agda}}: Updated Agda example) |
||
Line 546:
open import Data.Nat using (ℕ ; zero ; suc ; _*_)
factorial : (n : ℕ) → ℕ
factorial zero = 1
factorial (suc n) = (suc n) * (factorial n)
| |||