Skip to Content.
Sympa Menu

coq-club - Re: Re: [Coq-Club] How to project/define these attributes?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: Re: [Coq-Club] How to project/define these attributes?


chronological Thread 
  • From: zaman.a25 AT gmail.com
  • To: coq-club AT inria.fr
  • Subject: Re: Re: [Coq-Club] How to project/define these attributes?
  • Date: Mon, 8 Aug 2011 17:37:56 +0200

Thanks for your response. 

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



Archive powered by MhonArc 2.6.16.

Top of Page