Use where instead of var for expressions

[keyboardDrummer]

I don't like var expressions, because var is already used in statements so it can make code that is an expression look like a statement:

var x := ..
var y := ..
// are we inside an expression or a statement? it's impossible to tell from there
x := 3 // error: a let-bound variable can not be re-assigned. Aha, we were in an expression!

Also, while for statements the order of code affects the semantics, for expressions it does not, so it is no longer necessary for the definition of variables to come before their usage. I think it is more readable for the definition to come after the usage, since the name is used as a summary of the body, allowing one to read the code top-down.

I propose the following syntax:

function Foo(x: int): int =>
  x + y 
where 
  x := y + z;
  y := 2;
  z := 3;

Where bindings are checked for cyclic dependencies.

Note that I've also replaced the curly braces around the function body with a =>, which Dafny also uses as part of defining lambda expressions. I think this change makes it extra clear that the body of a function is not a statement. I think beginning Dafny users are often confused because they can not use statements inside function bodies, since the curly braces imply that they can.