[Agda] arguments in `data' pattern

[Ulf Norell]

On Sun, Jul 5, 2015 at 9:50 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:

> Can anyone explain, please,
> what is the matter with the attached (small) code?
>
> It includes
>
> -----------------------------------------------------------------
> data DecPrime : ℕ → Set      -- constructively decided primality
>      where
>      prime    : {n : ℕ} → IsPrime n → DecPrime n
>      unity    : DecPrime 1
>      composed : {m n : ℕ} → IsNontrivialDivisor m n → DecPrime n
>
> postulate  decPrime : (n : ℕ) → DecPrime n
>
> f : ℕ → ℕ
> f n = g n (decPrime n)
>       where
>       g : (m : ℕ) → DecPrime m → ℕ
>
>       g 1 unity                = 1
>       g _ (prime _)            = 2
>       g _ (composed {k} {_} _) = k
> ------------------------------------------------------------------
>

The first and the second underscores must be the same. You'll get an easier
to understand error if you replace the underscores with variables. This
checks:

   g m (composed {k} {.m} _) = k

It would make more sense to make the first argument to g hidden though.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150705/521e43aa/attachment.html