The Coq mailing list

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

>Jevgenijs Sallinens wrote 22 March 2004:
 > Structure Test : Set :=
 > {
 > X:Set
 > }.
 > Error: Large non-propositional inductive types must be in Type.


>Christine Paulin wrote 22 March 2004
>
> 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.
>

Many thanks to Christine Paulin for her perfect explanation.

I found it is possible in most  cases to replace records with modules
(module types).
In the mentioned example we just let.
Module Type Test.
  Parameter X:Set.
End Test.
In such manner I was able to overwrite large part of my previously announced
modular  development for natural numbers
and hope will be able to overwrite all of it.
There are only some complications with the usage of some tactics, since they
are not able to choose proper modules automatically,
but these are mostly technical problems..
There should be some theoretical implications: by replacing records with
modules we are able to remove explicit usage of universes Type_j,
so garanteed no problems like  'Universe Inconsistency'. Looks like 'Type'
is replaced by 'Module Type'
I just conjecture that  something similar could be achieved also within
traditional approach by reducing freedom in record usage to same level
as it is imposed by module mechanism.

Kind Regards,
Jevgenijs.