Parsing/Building : allow left arguments

I'm surprised we didn't do this earlier, but it would be a good quality of life to have left-hand-side arguments in definitions as such:

def foo (a b : A) (c : B) := ...

This shouldn't be too hard to implement, and would definitely help in making the code more reaable.