[Agda] moving common from `with'

[Dan Doel]

On Sun, Oct 14, 2012 at 7:08 AM, Serge D. Mechveliani <mechvel at botik.ru> wrote:
>> thus, there is no place to put a 'where' there.  Haskell's 'where' can
>> also be used in expressions.  But it allows funny stuff like
>>
>>   a = let x = 5
>>       in  x where x = 4
>>
>> Well, I could not tell whether the value of a should be 4 or 5 here...
>>
>> Adding 'where' to expressions has beend requested before...
>>
>
> I join this request.
> Concerning `let' and `where', Haskell has proved good.
> And it is desirable to follow Haskell in this point (as in many others).

No, Haskell's where cannot be attached to expressions. It is attached
to definitions exactly like Agda's. For instance, in the example
given, the 'where x = 4' is attached to the 'a =' definition, despite
the confusing layout. This is kind of obvious if you ask what a there
is: it's 5.

The difference in Agda is that expressions do not contain the type of
definitions that are allowed to have where attached in them. In
Haskell, any declaration in a let and any alternative in a case may
have a where attached. But this is not the case in Agda.

-- Dan