The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

Records in Coq are just a special notation for inductive definitions 
with automatic generation of projections functions

Structure Test : Set := { X:Set }.
defines
Inductive Test : Set := Build_Test : forall (X:Set), Test.
Typing rules for inductive definition applies
in particular the fact that each type of constructor in that case 
        forall (X:Set), Test
should be typed in an environment where Test : Set 
with the sort of the inductive definition in our case Set
Because in Coq V8.0, Set is not impredicative anymore
   Test : Set |- forall (X:Set), Test : Set 
doest not hold and the definition is rejected.

Christine Paulin


Jevgenijs Sallinens writes:
 > 
 > 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
 > 
 > --------------------------------------------------------
 > Bug reports: http://coq.inria.fr/bin/coq-bugs
 > Archives: http://pauillac.inria.fr/pipermail/coq-club
 >           http://pauillac.inria.fr/bin/wilma/coq-club
 > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  tel : (+33) (0)1 69 15 66 35         fax : (+33) (0)1 69 15 65 86