I am learning Idris and as a personal exercise, I would like to implement a Primes
type, consisting of all the prime numbers.
Is there a way in idris to define a new type starting from a type and a property, which will select all the elements of the starting type for which the property holds true? In my case, is there a way to define Primes
as the set of Nat
such that n <= p and n|p => n=1 or n=p
?
If this is not possible, should I define prime numbers constructing them inductively using some kind of sieve?
I like copumpkin's Agda definition of Prime, which looks like this in Idris:
Read as "if p is divisible by d, then d must be 1 or p" - a common definition for primality.
Proving this by hand for a number can be pretty tedious:
It's also very involved to write a decision procedure for this. That'll be a big exercise! You'll probably find the rest of the definitions useful for that:
https://gist.github.com/copumpkin/1286093