Zulip Chat Archive

Stream: new members

Topic: Easier work with triples


Martin Dvořák (May 23 2022 at 18:44):

I wrote the following definitions in order to work with triples more easily.

def first {α β γ : Type} (t : α × β × γ) : α := t.fst
def secon {α β γ : Type} (t : α × β × γ) : β := t.snd.fst
def third {α β γ : Type} (t : α × β × γ) : γ := t.snd.snd

What do I need to do in order to make it work with the "dot" notation?
I need to write third (1, 2, 3) now.
I'd rather write (1, 2, 3).third if possible.


Last updated: Dec 20 2023 at 11:08 UTC