The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

I think you are missing a piece of code:
you want to extract exactly one ProtocolEvent from your data, but
one of the constructors has two of them.

If I understand correctly, you either need to build a single ProtocolEvent
from these two (so you need to write a function to do so), or you have to
pick one of them en return it.

If you choose the first solution you will end up having something like:

| (Create_ProtocolEE p1 Bop p2) => Combine (GetpEvent p1) (GetpEvent p2)

(assuming your combining function is called Combine).
If you choose the last solution, you will end up having something like:

| (Create_ProtocolEE p1 Bop p2) => (GetpEvent p1)

Since we don't know much more about your ProtocolEvent structure, we
can't help you
combining them, this part is up to you.

Cheers,
Vincent

2011/8/10  
<zaman.a25 AT gmail.com>:
> Based on the following definition :
>
> Protocol : Set :=
> | Create_ProtocolB (pEvent: ProtocolEvent)
> | Create_ProtocolR (p:Protocol)(RepOp1: RepetitionOperator)
> | Create_ProtocolEE (p1: Protocol)(BinOp2: BinaryOperator)(p2: Protocol)
>
> I wish to define a function that will get the pEvent, given a Protocol as an
> input. Ive started it here:
>
> Fixpoint GetpEvent (p:Protocol) : ProtocolEvent :=
> match p with
> | (Create_ProtocolB pe) => pe  (*alias for pEvent*)
> | (Create_ProtocolR p1 Rop) => GetpEvent p1
> | (Create_ProtocolEE p1 Bop p2) => GetpEvent ...
> end.
>
> for the last clause, since it has two protocols, (p1 and p2), i dont know 
> how
> to tell the function to put p1 into the function (GetpEvent) to obtain its 
> pe,
> and then put p2 into the function with the argument p2. The GetpEvent 
> function
> i have defined only takes in one Protocol, so i dont know how to put both p1
> and p2 back into the function to evaluate their 'pe'. Even if i were to do 
> it
> one by one, i would be able to make the recursive call on the first; 
> GetpEvent
> p1. Dont know how to do it for the p2.
>