inc x y = x + y; five = inc (x := 3) 2;)
In fact in our case. for this to work the type annotation needs to be
inc: (x : Int) => Int -> Int;
Currently, yes. But we should also make it work if the type is
(x : Int) -> Int -> Int;
And, it should (once implemented) also work if there is no type annotation at all, because the inferred type would be
(x : Int) -> (y : Int) -> Int
Is this want we want ? The information seems quite redundant.
Not sure which redundancy you're referring to.
BTW, as you may have seen, I fixed conv_p (to some extent, at least), so now we actually do *check* the types, which caught various type errors in our code. I fixed some of them, but could you take a look at the remaining ones?
Stefan