[Agda] module _{a b}

[Sergei Meshveliani]

I do not know, this looks like a typo in Standard library
Data.List.All.Properties :

-- map

module _{a b} ...

(it works, though).

--
SM

[Matthew Daggitt]

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

Post by Sergei Meshveliani
I do not know, this looks like a typo in Standard library
-- map
module _{a b} ...
(it works, though).
--
SM
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda