I am always struck by the strange quirks of #Dafny imperative and functional syntax:
Take the syntax for function/method prototypes:
```
method Foo(a : int, b : int) returns (res : int)
function foo(a : int, b : int) : int
function fooAlt(a : int, b : int) : (res : int)
```
and now anonymous functions:
```
method Foo<A>(f : (A) -> B, a : A) returns (res : B)
```
I wish Dafny would have some sugar that harmonises the use of `->` above in favour of `:`. Colon implies 'has type' not returns a type...
```
Foo(a : int, b : int) -> (res : int)
```