The Coq mailing list

[zaman.a25 AT gmail.com]

Hi,

I have the Inductive definition:
Protocol : Set :=
| Create_ProtocolB (pEvent: ProtocolEvent)
| Create_ProtocolR (pR:Protocol)(RepOp1: RepetitionOperator)
| Create_ProtocolEE (protocol1: Protocol)(BinOp2: BinaryOperator)(protocol2:
Protocol) 

And wish to define the attribute projections, but Coq gives an error. How 
would
I define such attributes to get the ProtocolEvent (pEvent) of each Protocol?
Ive tried (for the attribute pEvent):

Definition pEvent : Protocol -> ProtocolEvent :=
(fun x: Protocol =>
match x with
| (Create_ProtocolB pe) => pe
| (Create_ProtocolR p r) => p
| (Create_ProtocolEE p1 bop p2) => p1
end).

I dont know how to define the attributes of a recursive Inductive definition. 

Thanks in advance.