Extract some element from a chained Product.

Stream: Is there code for X?

[Asei Inoue]

This is probably a question that has already been answered somewhere, but I could not find it.

def sample : Nat × Nat × Nat × Nat := (0, 1, 2, 3)

-- I want `2` from `(0, 1, 2, 3)`!

-- this does not work
#check_failure sample.3

-- this does not work
#check_failure sample[2]

[Mario Carneiro]

tuples are right-associative nested, there is no such thing as an n-ary tuple in lean

[Mario Carneiro]

so to get at the 2 in (0, 1, 2, 3) (which is really (0, (1, (2, 3)))) you should use sample.2.2.1

[Asei Inoue]

I think this API is inconvenient. Why not make it easier to access the nth in a chain of Prods?

[Andrew Yang]

Because we usually use Fin 4 -> Nat instead. There is the nice notation ![0, 1, 2, 3] for this.

[Asei Inoue]

oh thanks

[Asei Inoue]

where is ![]defined?

[Adam Topaz]

Mathlib.Data.Matrix.Notation I think

[Matt Diamond]

@Asei Inoue I think the ![] notation for Tuples is specifically defined in Mathlib.Data.Fin.VecNotation

[Matt Diamond]

there's also a lot of helper functions for Tuples in Mathlib.Data.Fin.Tuple.Basic and siblings, if you ever need to do something complex