The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

zaman.a25 AT gmail.com
 wrote:
> Ive written the following to get teh ProtocolEvent of the Protocols.
>
> Fixpoint pEvent (p:Protocol) : ProtocolEvent :=
> match p with
> | (Create_ProtocolB pe) => pe
> | (Create_ProtocolR p1 Rop) => pEvent p1 
> | (Create_ProtocolEE p1 Bop p2) => pEvent ..... ?
> end.
>
> For the last clause, how do I write so that it evaluates p1 first, and then
> evaluates p2?
>   

I don't understand the question, but it's probably worth pointing out 
that Coq has no inherent order of evaluation.  It isn't necessary, since 
all programs terminate.