[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