[Agda] moving common from `with'

Serge D. Mechveliani mechvel at botik.ru
Sun Oct 14 13:08:22 CEST 2012


On Sat, Oct 13, 2012 at 10:29:25PM +0200, Andreas Abel wrote:
> Agda's 'where' and 'let' are a bit different to Haskell's. 
>
> [..]
>
> 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).

Regards,
Sergei


More information about the Agda mailing list