coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: AUGER Cedric <Cedric.Auger AT lri.fr>
- To: Adam Chlipala <adamc AT csail.mit.edu>
- Cc: zaman.a25 AT gmail.com, coq-club AT inria.fr
- Subject: Re: [Coq-Club] How to project/define these attributes?
- Date: Mon, 8 Aug 2011 19:14:54 +0200
Le Mon, 08 Aug 2011 11:49:23 -0400,
Adam Chlipala
<adamc AT csail.mit.edu>
a écrit :
> zaman.a25 AT gmail.com
> wrote:
> > "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...
>
> You haven't given an unambiguous definition (even informally, in your
> list messages) of what behavior you want here. It sounds like what
> you are looking for is probably a basic recursive function.
>
> May I ask what source you're using to learn Coq? Most will introduce
> recursive functions quite early.
Or you can also learn it from almost any "ML" language, such as OCaml,
Haskell, and so on…
The only thing to know is the "Fixpoint" command name (see the
reference manual), or "fix" keyword if you really love the "Definition"
command name (see the same source).
- [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.