[Agda] primes

[Ruben Henner Zilibowitz]

Thanks. I think I found a better version of this anyhow:

-- Prime m is inhabited iff m is a prime number.
Prime : (m : ℕ) -> Set
Prime 0 = ⊥
Prime 1 = ⊥
Prime (suc (suc m)) = forall {i} -> i < (suc (suc m)) -> i Divides  
(suc (suc m)) -> i ≡ 1

Regards,

Ruben

On 12/03/2009, at 1:08 AM, Nils Anders Danielsson wrote:

> On 2009-03-11 13:48, Ruben Henner Zilibowitz wrote:
>
>> 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)"
>
> The problem is that Agda handles implicit arguments somewhat  
> strangely.
> I think your code will work if you write
>
> strictPrime2 : StrictPrime 2
> strictPrime2 = ⟨ (λ {_} → primetwo) , 2>1 ⟩
>
> instead.
>
> We should really improve the handling of implicit arguments.
>
> -- 
> /NAD
>
>
> This message has been checked for viruses but the contents of an  
> attachment
> may still contain software viruses, which could damage your computer  
> system:
> you are advised to perform your own checks. Email communications  
> with the
> University of Nottingham may be monitored as permitted by UK  
> legislation.
>