Factorial: Difference between revisions
Content added Content deleted
No edit summary |
|||
| Line 542: | Line 542: | ||
=={{header|Agda}}== |
=={{header|Agda}}== |
||
<syntaxhighlight lang="agda"> |
<syntaxhighlight lang="agda">module Factorial where |
||
open import Data.Nat using (ℕ ; zero ; suc ; _*_) |
|||
factorial : ℕ → ℕ |
|||
factorial zero = 1 |
factorial zero = 1 |
||
factorial (suc n) = suc n * factorial n |
factorial (suc n) = (suc n) * (factorial n) |
||
</syntaxhighlight> |
|||
=={{header|Aime}}== |
=={{header|Aime}}== |
||