Discussion:
module _{a b}
(too old to reply)
Sergei Meshveliani
2018-03-10 20:28:01 UTC
Permalink
Raw Message
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
2018-03-10 23:10:59 UTC
Permalink
Raw Message
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
Loading...