The Coq mailing list

["Jevgenijs Sallinens" <jevgenijs AT dva.lv>]

Dear Coq Users and Developers,

Me and probably many others Coq users would be interested in more
information on the theory behind Coq.
Are there others sources available except Coq Reference Manual?
Especialy I am interested in the complete list of
inference rules for Coq8.0.
For example, I was unable to find in the Manual what is the theory behind
records (structures). In Z.Luo's ECC there are special inference rules for
Sigma-types, which seems are absent in the Coq Manual.
In particular seems no explanation what are general rules to avoid
situations like following:
Structure Test : Set :=
{
X:Set
}.
Error: Large non-propositional inductive types must be in Type.

Thanks in advance for any kind of additional information.

Jevgenijs.


________________________________________________
Message sent using UebiMiau 2.7.2