[Agda] question about with

[Nils Anders Danielsson]

On Fri, Feb 29, 2008 at 8:45 PM, Ulf Norell <ulfn at cs.chalmers.se> wrote:
>
> What happens is that n is abstracted also from the type of plus-lh-z'

One could imagine having support for selecting exactly which
occurrences of the given expression to abstract over. However, this
seems a bit heavy-weight, especially since the task can already be
accomplished by using a helper function.

-- 
/NAD