3 ms·
The constructive nature of Idris makes it hard (at least for me) to express a prime under 1,000,000 as a type. For example, it's trivial to express a composite
by kestert 12y ago
The constructive nature of Idris makes it hard (at least for me) to express a prime under 1,000,000 as a type. For example, it's trivial to express a composite as a GADT:
data Composite : Nat -> Type where
factors : (x : Nat) -> (y : Nat) -> Composite ((S (S x)) * (S (S y)))
but there is no analogous construction of a prime type. Luckily most day to day programming looks more like the composite case than the prime case.
- gergoerdi 12y agoAs an example, here's how primality is defined in the Agda standard library. It is simply the negation of the property 'has a divisor and is greater than 2'. http://agda.github.io/agda-stdlib/html/Data.Nat.Primality.html http://agda.github.io/agda-stdlib/html/Data.Nat.Primality.ht...