Dependent Tuple in Idris?

Question

It's easy to write down a dependent pair in Idris with the "**" syntax sugar:

data Positive : Int -> Type where
    OneIsPositive : Positive 1
    SucIsPositive : Positive i -> Positive (i+1)

data IsEven : Int -> Type where
    ZeroIsEven : IsEven 0
    Add2IsEven : IsEven i -> IsEven (i+2)
    Sub2IsEven : IsEven i -> IsEven (i-2)

v1 : (x : Int ** Positive x)
v1 = (1 ** OneIsPositive)

v2 : (x : Int ** IsEven x)
v2 = (2 ** Add2IsEven ZeroIsEven)

But When I want to put more things into the tuple, I failed (the following code causes error):

v3 : (x : Int ** Positive x ** IsEven x)
v3 = (2 ** SucIsPositive OneIsPositive ** Add2IsEven ZeroIsEven)

So, generally, what should I do when I want to put more than 2 element into the Dependent Pair (Tuple) ?

---

I find that I can use a nested normal tuple to do that in this case:

v3 : (x : Int ** (Positive x, IsEven x))
v3 = (2 ** (SucIsPositive OneIsPositive, Add2IsEven ZeroIsEven))

But this is limited. When the third part is depending on the second one, this no longer works.

So I'm still wondering what is the suggested way to do that?

Answer 1

If the type of the third component of your dependent tuple does not depend on the value of the second component, then non-dependent pair as you have shown is the way to go.

In case you want a nested dependent pair you need to give a name to the second component:

v3 : (x : Int ** unusedName : Positive x ** IsEven x)