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

[Ulf Norell]

On Wed, May 14, 2008 at 6:09 PM, Samuel Bronson <naesten at gmail.com> wrote:

> 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.)


Fixed. Make case (C-c C-c) should now also work in 'with'-clauses. Beware
that only the current line will be replaced when making case, so hitting C-c
C-c here:

foo a b c
   = {! b !}

will result in something like

foo a b c
   foo a zero c = ?
   foo a (suc n) c = ?

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080515/55bd4661/attachment-0001.html