[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