The Coq mailing list

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