[Agda] nameless pattern-matching functions

[Nils Anders Danielsson]

On Sat, Mar 8, 2008 at 12:46 AM, Dan Licata <drl at cs.cmu.edu> wrote:
>
>  But agda already doesn't let me refine outer scope variables in a helper
>  function, at least in this instance:

This can sometimes be annoying, requiring large refactorings. I have
requested that this restriction should be relaxed:

http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Main.ModuleSystemMoreFlexible

(Note that where clauses are syntactic sugar for modules parameterised
on the variables bound on the left hand side.)

-- 
/NAD