Idris - determining the type of primes

Question

I study Idris and as a personal exercise, I would like to implement a type Primesconsisting of all prime numbers.

Is there an idris way to define a new type, starting with a type and a property that will select all elements of the original type for which the property is true? In my case, is there a way to determine Primeshow a set is Natsuch that n <= p and n|p => n=1 or n=p?

If this is not possible, should primes be constructed inductively using a sieve?

Answer 1

I like the copumpkin Agda definition of Prime , which looks like this in Idris:

data Divides : Nat -> Nat -> Type where
  MkDivides : (q : Nat) ->
              n = q * S m ->
              Divides (S m) n

data Prime : Nat -> Type where
  MkPrime : GT p 1 ->
            ((d : Nat) -> Divides d p -> Either (d = 1) (d = p))
            -> Prime p

" p d, d 1 p" - .

:

p2' : (d : Nat) -> Divides d 2 -> Either (d = 1) (d = 2)
p2' Z (MkDivides _ _) impossible
p2' (S Z) (MkDivides Z Refl) impossible
p2' (S Z) (MkDivides (S Z) Refl) impossible
p2' (S Z) (MkDivides (S (S Z)) Refl) = Left Refl
p2' (S Z) (MkDivides (S (S (S _))) Refl) impossible
p2' (S (S Z)) (MkDivides Z Refl) impossible
p2' (S (S Z)) (MkDivides (S Z) Refl) = Right Refl
p2' (S (S Z)) (MkDivides (S (S _)) Refl) impossible
p2' (S (S (S _))) (MkDivides Z Refl) impossible
p2' (S (S (S _))) (MkDivides (S _) Refl) impossible

p2 : Prime 2
p2 = MkPrime (LTESucc (LTESucc LTEZero)) p2'

. ! , :

https://gist.github.com/copumpkin/1286093