[Agda] Defining a module by pattern matching

Nils Anders Danielsson nad at cse.gu.se
Wed May 15 22:14:18 CEST 2013


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


More information about the Agda mailing list