Why does Adam Chlipala use left-associated nested tuples to represent Ltac lists in CPDT?

1
votes

Via CpdtTactics.v:

[...] Succeed iff x is in the list ls, represented with left-associated nested tuples.

Ltac inList x ls := match ls with | x => idtac | (_, x) => idtac | (?LS, _) => inList x LS end.

This seems atypical. Doesn't the tail of the list conventionally go in the right-hand side of the tuple?

2
listcoqltac

2 Answers

3
votes

Via private communication with Adam:

No, I can't think of any way to prefer one version over the other, actually. I just had to make some choice for that part of the book.

2
votes

Somehow n-tuples are nested pairs associated to the left:

(x, y, z)

desugars to

pair (pair x y) z

And that's what we get if we want to write inList x (x, y, z).