Zulip Chat Archive

Stream: new members

Topic: functions with pairs as arguments

Jeremy Teitelbaum (Dec 08 2021 at 19:44):

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 (Dec 08 2021 at 19:45):

Looks right to me

Jeremy Teitelbaum (Dec 08 2021 at 19:47):

function expected at
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 (Dec 08 2021 at 19:47):

Sounds like there is something below the line which interferes

Jeremy Teitelbaum (Dec 08 2021 at 19:48):

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

Jeremy Teitelbaum (Dec 08 2021 at 19:50):

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

Johan Commelin (Dec 08 2021 at 19:56):

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.

Last updated: Dec 20 2023 at 11:08 UTC