[Agda] primes

[Julian Beaumont]

Hey Ruben,

In the definition

exPrimes : ∃ Prime
exPrimes = 2 , 2-prime

agda applies 2-prime to implicit arguments before trying to typecheck
it, so you end up with something equivalent to

exPrimes : ∃ Prime
exPrimes = 2 , (2-prime {_})

You can see now that (2-prime {_}) doesn't have type Prime 2, hence
the error message. To get around this you need to do something like

exPrimes : ∃ Prime
exPrimes = 2 , (λ {_} → 2-prime)


Julian.

On Sun, Nov 1, 2009 at 4:58 PM, Ruben Henner Zilibowitz
<rzilibowitz at yahoo.com.au> wrote:
> Hi. I'm using Agda 2.2.4 on Emacs. Here is a module I wrote:
>
> -------------
>
> module Test where
>
> open import Data.Nat
> open import Data.Nat.Divisibility
> open import Data.Empty
> open import Relation.Binary.PropositionalEquality
> open import Relation.Nullary.Negation
> open import Data.Fin using (fromℕ≤)
> open import Relation.Nullary
> open import Data.Product
>
> -- Prime m is inhabited iff m is a prime number.
> Prime : (m : ℕ) → Set
> Prime 0 = ⊥
> Prime 1 = ⊥
> Prime m = forall {i} → i < m → i ∣ m → i ≡ 1
>
> sn≢0 : ∀ {n} → (suc n) ≢ 0
> sn≢0 ()
>
> 2-prime : Prime 2
> 2-prime (s≤s z≤n) 0|2 = contradiction (0∣0 0|2) sn≢0
> 2-prime (s≤s (s≤s z≤n)) _ = refl
>
> exPrimes : ∃ Prime
> exPrimes = 2 , 2-prime
>
> -------------
>
> It chokes on the last line with the error:
>
> /Users/rhz/Documents/dev/Agda/Test.agda:26,16-23
> (_27 < suc (suc 0) → _27 ∣ suc (suc 0) → _27 ≡ 1) !=
> ({i : ℕ} → i < suc (suc 0) → i ∣ suc (suc 0) → i ≡ 1) because one
> is an implicit function type and the other is an explicit function
> type
> when checking that the expression 2-prime has type Prime 2
>
> Could someone explain this error to me?
>
> Thanks,
>
> Ruben
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>