The Coq mailing list

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

zaman.a25 AT gmail.com
 wrote:
> "the second two pattern matching cases clearly aren't returning
> [ProtocolEvent]s."
>
> Exactly. Coq is requiring me to define all cases in the pattern matching. How
> would I get the ProtocolEvents of the other two cases?  I just want to be able
> to get the pEvent of the Protocols: pR, Protocol1 and Protocol2... 
>   

You haven't given an unambiguous definition (even informally, in your 
list messages) of what behavior you want here.  It sounds like what you 
are looking for is probably a basic recursive function.

May I ask what source you're using to learn Coq?  Most will introduce 
recursive functions quite early.