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