Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: zaman.a25 AT gmail.com
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] How to project/define these attributes?
  • Date: Wed, 10 Aug 2011 09:24:12 -0400

zaman.a25 AT gmail.com
 wrote:
Ive written the following to get teh ProtocolEvent of the Protocols.

Fixpoint pEvent (p:Protocol) : ProtocolEvent :=
match p with
| (Create_ProtocolB pe) => pe
| (Create_ProtocolR p1 Rop) => pEvent p1 | (Create_ProtocolEE p1 Bop p2) => pEvent ..... ?
end.

For the last clause, how do I write so that it evaluates p1 first, and then
evaluates p2?

I don't understand the question, but it's probably worth pointing out that Coq has no inherent order of evaluation. It isn't necessary, since all programs terminate.



Archive powered by MhonArc 2.6.16.

Top of Page