Factorial: Difference between revisions

Content added Content deleted
No edit summary
Line 542:
 
=={{header|Agda}}==
<syntaxhighlight lang="agda">factorialmodule :Factorial ℕ → ℕwhere
 
open import Data.Nat using (ℕ ; zero ; suc ; _*_)
 
factorial : ℕ → ℕ
factorial zero = 1
factorial (suc n) = (suc n) * (factorial n</syntaxhighlight>)
</syntaxhighlight>
 
=={{header|Aime}}==
Retrieved from "https://rosettacode.org/wiki/Factorial"