Zulip Chat Archive

Stream: new members

Topic: how to destructure tuple in function definition


Kevin Tran (Sep 08 2020 at 14:32):

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 (Sep 08 2020 at 14:37):

Use \< \>

Johan Commelin (Sep 08 2020 at 14:37):

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

Kevin Tran (Sep 08 2020 at 14:40):

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

Kevin Tran (Sep 08 2020 at 14:43):

\< \a \>

Reid Barton (Sep 08 2020 at 14:43):

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 (Sep 08 2020 at 14:48):

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

Reid Barton (Sep 08 2020 at 14:48):

I copied and pasted them from a Lean file

Kevin Tran (Sep 08 2020 at 14:50):

zulip doesn't have markup for greek letters?


Last updated: Dec 20 2023 at 11:08 UTC