The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

Ah, version 8.4 includes vectors... my bad nevermind about that. Thanks you guys :)

On Sun, Nov 11, 2012 at 6:03 PM, Kenneth Adam Miller <kennethadammiller AT gmail.com> wrote:

Thank you so much, Pierre, for a direct and specific answer. And for the additional links! :)

But I have a problem in that I can't do Require Vector in the version of CoqIDE that I'm tied to (8.3pl2). I get an error: Cannot find library Vector in loadpath

On Sun, Nov 11, 2012 at 4:13 PM, Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr> wrote:

Hi,
the purpose is to write this module in the Ocaml style. It means that you mustn't Import this module.
You only
Require Vector.
then you write as in Ocaml Vector.hd, Vector.nth Vector.fold_left … (This is supposed to be the meaning of the first comment. Maybe, I should rephrase it.) So as in Ocaml, the data structure defined in the module Module has name Module.t.

As far as I don't understand C, you want a kind of http://coq.inria.fr/distrib/V8.4/stdlib/Coq.Init.Datatypes.html#sum

At last, I would say that someone new to Coq will find answers in
http://adam.chlipala.net/cpdt/
and in
http://www.cis.upenn.edu/~bcpierce/sf/
French/chinese speaking people use http://www.labri.fr/perso/casteran/CoqArt/ but english people have to buy it/go to the library …

All the best,
Pierre B

Le 11 nov. 2012 à 21:52, <kennethadammiller AT gmail.com> a écrit :

> So, after looking at the vector specification at
> http://coq.inria.fr/distrib/V8.4beta/stdlib/Coq.Vectors.VectorDef.html#
> I'm lost as to why t was used in place of vector. Why would the designers
> choose t instead of vector?
>
> Also, as part of an assignment, I have to model some C unions in Coq-I'm new
> to Coq, so I was wondering what data type I would use to get this done.