[Agda] `abstract' fail

[Andrea Vezzosi]

It does seem like a bug where the pattern matching lambda gets
desugared outside the abstract block.


Best,
Andrea

On Sun, Oct 4, 2015 at 11:35 PM,  <mechvel at scico.botik.ru> wrote:
> Can people tell, please,
>
> why in the  _attached code_  `abstract' is not allowed in  Agda 2.4.2.4 ?
>
> half-n=n-div-2   is implemented via `case'.
>
> If it is not under `abstract', then it is type checked.
>
> Is this a bug in Agda ?
>
> Thanks,
>
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>