The Coq mailing list

[Alexandre Miquel <miquel AT ausone.inria.fr>]

On Tue, Feb 13, 2001 at 09:03:06AM -0100, Carlos.SIMPSON wrote:
> Hi. I'm sorry if this is a redundant question since I just signed up
> for the discussion list. Is there any way to make explicit the
> indexation of the hierarchy of Type (i.e. the index i in Type(i))
> when using Coq?  This would seem to be necessary in order to correctly
> fix the meaning of statements dealing with different universes.
> 
> Thanks---
> Carlos Simpson
>
Today, there is no way for explicitly indexing the Type's in the
universe hierarchy of Coq.  (It seems difficult to add this feature
into the existing machinery, which is already tricky since it must take
care about sectionning and separate compilation.)

However, I recently used the following trick for explictly naming
universes.  Suppose you want to work with universes Type(1), Type(2)
Type(3) and Type(4) for example.  (The precise indices generally
don't matter, since we are more interested by their relative
positions into the hierarchy.)  We can explicit such constraints
by simply writing

  Definition Type4 := Type.
  Definition Type3 : Type4 := Type.  (* make [Type3 : Type4] explicit *)
  Definition Type2 : Type3 := Type.  (* etc. *)
  Definition Type1 : Type2 := Type.

and by using the constants Type1, Type2, Type3 and Type4 in the
following, instead of the anonymous sort Type.

This trick does not solve all the problems, but it is still useful
for debugging.  Since constraints are set up from the beginning, we
are sure that Coq will not (silently) add a constraint which could
be inconsistent with the constraints we have in mind.  Experience
shows that the "Universe Inconsistency" exception is then raised at
the precise place we have done the mistake in the development, and
not 18 definitions later... so we can easily fix it.

Hope this helps...


-- Alexandre Miquel  
<Alexandre.Miquel AT inria.fr>