[Agda] arguments in `data' pattern

[Andreas Abel]

Incidentially, this is an instance of what I discuss in my message

  [Agda] Should not _ patterns be resolvable by inaccessible patterns?

On 05.07.2015 22:38, Ulf Norell wrote:
>
>
> On Sun, Jul 5, 2015 at 9:50 PM, Sergei Meshveliani <mechvel at botik.ru
> <mailto: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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/