[Agda] Re: Data.Nat.Primality.Prime and irreducibility

[Dr. ÉRDI Gergő]

On Mar 7, 2015 3:44 PM, "N. Raghavendra" <raghu at hri.res.in> wrote:
> However, I should've said that,
> in any case, 0 is not irreducible by the general definition because
> 0=0*0, and neither of the two factors 0 and 0 on the right hand side is
> a unit in Nat.

Touchè.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150307/86258c08/attachment.html