[Agda] Eta reduction of a function argument in a where block

[Nils Anders Danielsson]

On 2011-08-08 15:48, Wojciech Jedynak wrote:
> OK, now I know what is my question :-) Would it be possible to have
> Agda automagically simplify the helper module so the main functions'
> (here f1) arguments that are not used in f2 are not abstracted upon?

I have also been bitten by problems like the one you describe. However,
pruning the module telescope in the way you suggest does not seem to fit
well with interactive development. If the body of f₂ is initially a
goal, should the pattern variables of f₁ not be in scope in the goal? Or
should we delay the pruning until there are no unsolved meta-variables
in the where module, thus making it hard to write subsequent code
concurrently with f₂?

Fortunately it is easy to work around the problem: you can write the
where module yourself, and gain complete control over it.

-- 
/NAD