[Agda] module _{a b}

[Matthew Daggitt]

Yes, you're right. There could be a space there. I'll add it in at some
point. Nice spot.

On Sat, Mar 10, 2018 at 8:28 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> I do not know, this looks like a typo in Standard library
> Data.List.All.Properties :
>
>  -- map
>
>  module _{a b} ...
>
> (it works, though).
>
> --
> SM
>
> _______________________________________________
> 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/20180310/56386434/attachment.html>