The Coq mailing list

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

zaman.a25 AT gmail.com
 wrote:
> 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).
>   

From your prose description, it isn't clear to me what you mean to do.  
The above code doesn't make sense to me as "a way of getting the 
ProtocolEvent of a Protocol," since the second two pattern matching 
cases clearly aren't returning [ProtocolEvent]s.

Perhaps the answer to your question is that you are thinking too Lisply 
and should be prepared to use explicit pattern matching throughout your 
code, rather than writing "attribute projection" functions once?  I 
believe that would be the most idiomatic style, but you could also 
implement "projections" that return [option] types, yielding [None] when 
the projection doesn't make sense for its actual argument.  Yielding a 
safe default value in inapplicable cases would be a further option, 
which would bother most Coq users even more, on stylistic grounds. ;)

P.S.: None of the parentheses in your [pEvent] definition are needed.