how to destructure tuple in function definition

Stream: new members

[Kevin Tran]

how do i write a function that takes in a tuple, but destructured? something like

def uncurry (f : \a \to \b \to \g) := fun (a, b), f a b

[Johan Commelin]

Use \< \>

[Johan Commelin]

But lean needs to know the expected type. You are giving it very little info atm

[Kevin Tran]

sorry, i don't understand how to use \< and \>. could you give an example?

[Kevin Tran]

\< \a \>

[Reid Barton]

def uncurry (f : α → β → γ) : α × β → γ := λ ⟨a, b⟩, f a b

(a, b) isn't supported as the argument of a lambda. Therefore you also have to tell Lean the expected type of the function.

[Kevin Tran]

oh i get it now instead of ( and ) use \< and \>. also how did you type in the nice looking alpha and beta?

[Reid Barton]

I copied and pasted them from a Lean file

[Kevin Tran]

zulip doesn't have markup for greek letters?