The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Mon, 08 Aug 2011 11:49:23 -0400,
Adam Chlipala 
<adamc AT csail.mit.edu>
 a écrit :

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

Or you can also learn it from almost any "ML" language, such as OCaml,
Haskell, and so on…
The only thing to know is the "Fixpoint" command name (see the
reference manual), or "fix" keyword if you really love the "Definition"
command name (see the same source).