[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:



More information about the Agda mailing list