[Agda] Defining a module by pattern matching

[Nils Anders Danielsson]

On 2013-05-15 21:05, Guillaume Brunerie wrote:
> Is there a way to workaround this issue? Some way to define a
> parametrized module by pattern matching, or something like that?

I noted this problem in a feature request back in 2007, before we
started using the bug tracker:

   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.ModuleSystemMoreFlexible

-- 
/NAD