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

[Nils Anders Danielsson]

On 2011-08-07 19:38, Wojciech Jedynak wrote:
> I have been playing with Martin-Loef's W-types and I noticed a strange
> Agda behavior while using the recursor for W-flavored naturals.
> I think that in one of the cases in the code below, a function defined
> in a where block receives an additional parameter when it's not
> supposed to.

If you define

   f₁ args₁ = body₁
     where
     f₂ : Type
     f₂ args₂ = body₂

then Agda behaves as if you wrote (roughly) the following code:

   mutual

     f₁ args₁ = body₁[f₂ ≔ _M.f₂ <pattern variables from args₁>]

     module _M <typed pattern variables from args₁> where

       f₂ : Type
       f₂ args₂ = body₂[f₂ ≔ _M.f₂ <pattern variables from args₁>]

You can even give the module's name explicitly:

   f₁ args₁ = body₁
     module M where
     f₂ : Type
     f₂ args₂ = body₂

-- 
/NAD