The Coq mailing list

[zaman.a25 AT gmail.com]

Thanks.

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?

Thanks in advance.