[Agda] Many ways to open a module - Is there a reason?

[Apostolis Xekoukoulotakis]

If the module is a record, we use

"open Pair p"

If it is a simple module

"open B"

if it is a parametrized module

"module C = B a
 open C"

or

"open module C = B a"


I find that all these different ways to open a module complicate things.
I would prefer if there was a single concept and that reflected into a
uniform way of opening a module.

For example, every module is a record.
A parametrized module is a parametrized record.

And omit "Pair". Just write:
"open p"

or

"open (p a)".
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170330/7955c713/attachment.html>