functions with pairs as arguments

Stream: new members

[Jeremy Teitelbaum]

I want a function that takes an ordered pair of natural numbers and returns their sum. Why is this wrong?

def mysum (x : ℕ × ℕ ) : ℕ := x.1 + x.2

[Rob Lewis]

Looks right to me

[Jeremy Teitelbaum]

function expected at
x.snd
term has type
ℕ
Additional information:
/home/jet08013/GitHub/formalising-mathematics/src/experiments.lean:26:34: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
too many arguments

[Yaël Dillies]

Sounds like there is something below the line which interferes

[Jeremy Teitelbaum]

Maybe I'm invoking it incorrectly? How should I call this function?

[Jeremy Teitelbaum]

I'm an idiot. I forgot #eval and just wrote ff(2,3) below it....

[Johan Commelin]

In case something like this happens again, note that you can always write a . or #exit on the line below your lemma to make sure Lean doesn't only looks at line n that you care about and doesn't get confused by whatever is written on line n+1 and onwards.