[Agda] C-c C-c not working with module parameters or explicit cases over implicit arguments...

Samuel Bronson naesten at gmail.com
Wed May 14 18:09:06 CEST 2008


When working in a module with a parameter, C-c C-c keeps trying to
pattern match on that parameter...

Also, if I explicitly request a case over an implicit parameter, it
generates the cases but forgets to pattern match on the parameter.
(For instance, when implementing Reflexive properties.)


More information about the Agda mailing list