The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Thu, 15 May 2014 23:23:49 +0200,
Marcus Ramos 
<marcus.ramos AT univasf.edu.br>
 a écrit :

> Hi,
> 
> Can anyone suggest me a good tutorial on "Record" (definition, usage
> and examples)?
> 
> Thanks in advance,
> Marcus.

What do you expect to learn on "Record"?

I find this request a little strange, as I am pretty sure that Record
is almost the same thing as Inductive with the following tweaks:
- automatic generation of projections
- alternative syntax for builder

I do not remember if the notations and the 'let' definitions inside of
records are documented, beside that, I really do not see much to say
on records (unlike "Class" which is internally a record, but has other
interesting features record does not have).

Note that the system sadly does not allow you to define recursive
records, so do not expect to define things like:

Record tree := Node
  { index : Type;
    subtrees : index -> tree
  }.

or

Record nlist (A : Type) := N
  { head : A;
    tail : tlist
  }
with tlist (A : Type) :=
  | TNil : tlist A
  | TCons : nlist À -> tlist A.