The Coq mailing list

[Justus Matthiesen <justus.matthiesen AT cl.cam.ac.uk>]

> I'm lost as to why t was used in place of vector. Why would the designers
> choose t instead of vector?

It's a convention in OCaml to give the name "t" to the main data structure 
implemented in a file/module. I guessed it's spilled over into the Coq 
standard library in places.


> 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.

Have you tried the "Software Foundations" book [1] by Benjamin Pierce et al.? 
The first few sections of the first chapter should give you enough 
information 
to answer your assignment.


Justus

[1] http://www.cis.upenn.edu/~bcpierce/sf/