Problems with multi-arg lambdas

[benmos]

With HEAD as of this morning, I get the following error when trying to use a multi-arg lambda at the REPL:

*test> (\x, y => x + y) 3 2
(input):1:INTERNAL ERROR: "Nothing to introduce"
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/edwinb/Idris-dev/issues

*test> (\x, y => x `plus` y) 3 2
(input):1:INTERNAL ERROR: "Nothing to introduce"
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/edwinb/Idris-dev/issues

[edwinb]

Hmm, this one is old, I'm surprised I didn't comment because it's at least easy to explain, if not to fix... Lambdas only work if they have a type, so type directed elaboration doesn't work here. It's okay if you give it a type, but I realise it's a bit awkward:

let f : (Nat -> Nat -> Nat) = (\x, y => x + y) in f 3 2

[edwinb]

This appears to have been fixed a while ago (probably while fixing a different issue).