coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] How to project/define these attributes?, zaman . a25
- Re: [Coq-Club] How to project/define these attributes?, Adam Chlipala
- <Possible follow-ups>
- Re: Re: [Coq-Club] How to project/define these attributes?,
zaman . a25
- Re: [Coq-Club] How to project/define these attributes?,
Adam Chlipala
- Re: [Coq-Club] How to project/define these attributes?, AUGER Cedric
- Re: [Coq-Club] How to project/define these attributes?,
Adam Chlipala
- Re: Re: [Coq-Club] How to project/define these attributes?,
zaman . a25
- Re: [Coq-Club] How to project/define these attributes?, Adam Chlipala
- Re: Re: [Coq-Club] How to project/define these attributes?,
zaman . a25
- Re: Re: [Coq-Club] How to project/define these attributes?, Vincent Siles
- Re: Re: Re: [Coq-Club] How to project/define these attributes?,
zaman . a25
- Re: [Coq-Club] How to project/define these attributes?, Adam Chlipala
Archive powered by MhonArc 2.6.16.