[Agda] documentation for ".."

[Ulf Norell]

I think the rules aren't nailed down precisely (or documented), but the
compiler treats ".." as "erase at runtime". A consequence is that you
cannot pattern match on a ".." argument

In this particular case it means that the 'n' will not be an argument to
the constructors at runtime.

/ Ulf

On Thu, Sep 8, 2016 at 10:28 PM, Martin Stone Davis <
martin.stone.davis at gmail.com> wrote:

> I'm curious about a certain syntax involving "..". E.g., from the
> agda-prelude:
>
> data Fin : Nat → Set where
>   zero : ∀ ..{n} → Fin (suc n)
>   suc  : ∀ ..{n} (i : Fin n) → Fin (suc n)
>
> Where can I learn more about this? I didn't find it in the CHANGELOG or
> the official User Manual. Was it discussed on this list perhaps?
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160909/99432c25/attachment.html