listcoqltac

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

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?

Solution

  • 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).