The Coq mailing list

[Joshua Gancher <jrg358 AT cornell.edu>]

Hi all,

I am mechanizing a program logic, and have an equivalence judgement (written as an Inductive) of the form Equiv xs xs', where xs and xs' are of the type list Cmd. 

My current way of displaying this goal looks something like [:: p1; p2; p3; p4] <~~> [:: p5; p6; p7] (using ssreflect's notation for lists.) I would like to instead display something like:

0 : p1;

1 : p2;

2 : p3;

4 : p4

<~~>

0 : p5;

1 : p6;

2 : p7.

Is there a simple programmatic way of doing this, akin to defining a pprint_equiv : forall xs xs', Equiv xs xs' -> string? I think I could also achieve this by zipping each list with an increasing sequence of nats, and doing something special with this list of pairs, but this seems overkill if there is a more natural solution.

Thanks,

Joshua