RFC: binders for tuple components in function prototype
It would be useful if we could name tuple components in function prototypes e.g.
val f (x: int, y: int) : (r: int)
requires { x < 0 && y > 0 }
ensures { r = x + y }
Currently, we have to bind the tuple and then decompose it in every clause of the contract:
val f (p: (int, int)) : (r: int)
requires { let x, y = p in x < 0 && y > 0 }
ensures { let x, y = p in r = x + y }