The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

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.