[Agda] primes

[Lennart Augustsson]

Can't you just add a condition (m > 1)?

On Wed, Mar 11, 2009 at 1:13 PM, Ruben Henner Zilibowitz
<rzilibowitz at yahoo.com.au> wrote:
> Hi,
>
> I'm having some difficulty finding a type that expresses "m is a prime
> number".
>
> Here is what I've got:
>
> -- Prime m is inhabited iff m is a prime number or 0 or 1.
> Prime : (m : ℕ) -> Set
> Prime m = forall {i} -> i < m -> i Divides m -> i ≡ 1
>
> The problem is that 0 and 1 shouldn't be prime numbers but under this
> definition they are. So far I haven't been able to figure out something
> better. Any suggestions would be great.
>
> Regards,
>
> Ruben
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>