Why are these two tuples in idris equal?

Question

I am reading a Type driven development with Idris , and one of the exercises asks the reader to define a type TupleVectsuch that the vector can be represented as:

TupleVect 2 ty = (ty, (ty, ()))

I solved it by specifying the following type:

TupleVect : Nat -> Type -> Type
TupleVect Z ty = ()
TupleVect (S k) ty = (ty, TupleVect k ty)

The following test typeschecks:

test : TupleVect 4 Nat
test = (1,2,3,4,())

My question is why (1,2,3,4,()) == (1,(2,(3,(4,()))))? I would think that the right side is a 2-tuple consisting of Intand another tuple.

Answer 1

By checking the documentation at http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#tuples , you can see that the tuples are represented as nested pairs.

Consequently, (x, y, z) == (x, (y, z))for each x, y,z