The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Hi, all; I wrote this file; I have no question about what I did, but It  
may interest some of you about modules, records, mutual reflexivity and  
extraction; and find examples.
There is no explanation on how it works/doesn't work, just understand by  
yourself.
Use "ocamldoc meta.v" to get an html version.

About records, why is the following syntax defined but not documented in  
the Coq manual?
I know, it can be useful:

Variable A : Type.
Variable a : A.
Variable equiv : A -> A -> Prop.
Variable foofoo : A -> Prop.

Record foo (barfoo: A) :=
{ bar := a;
  foobar : equiv bar barfoo;
  barbar : foofoo bar
}

then

Definition get_alias_bar bf (f : foo bf) := bar f.

Yes, you can define "let" in records and use it as a field!

I didn't used it in my file, but you can if you want, there are some  
interesting places.

Attachment: meta.v
Description: Binary data