[Agda] primes

[Ruben Henner Zilibowitz]

What do you mean by "add a condition"?

I tried this:

-- 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

StrictPrime : (m : ℕ) -> Set
StrictPrime m = (Prime m) & (m > 1)

primetwo : Prime 2
primetwo (s≤s z≤n) ()
primetwo (s≤s (s≤s z≤n)) _ = refl

2>1 : 2 > 1
2>1 = s≤s (s≤s z≤n)

strictPrime2 : StrictPrime 2
strictPrime2 = ⟨ primetwo , 2>1 ⟩

However strictPrime2 does not type check. I get an error message I  
don't understand:
"suc _66 ≤ 2 → _66 Divides 2 → ..Relation.Binary.Core._._≡_ _66  
1 !=
{i : ℕ} → suc i ≤ 2 → i Divides 2  
→ .Relation.Binary.Core._._≡_ i 1
because one is an implicit function type and the other is an
explicit function type
when checking that the expression ⟨ primetwo , 2>1 ⟩ has type
({i : ℕ} →
  suc i ≤ 2 → i Divides 2 → ..Relation.Binary.Core._._≡_ i 1)
& (2 ≤ 2)"

Regards,

Ruben

On 12/03/2009, at 12:33 AM, Lennart Augustsson wrote:

> 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
>>