[Agda] primes

[Nils Anders Danielsson]

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.