The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Jeffrey Terrell wrote:
> I have a few questions about the type Type.
>
> 1.  What is the significance of Top in Type annotations? Is Type (* 
> (0)+1 *) the same as Type (* (Top.0)+1 *)?

I think my answer to this question should also address the next two.

The term [(0)] represents the lowest type universe.  Any term of the 
form [(Module.number)] represents a mutable universe _variable_.  That 
is, the answer to your question is no.  Think of the first as a constant 
and the second as a variable that just happens to contain the constant 
in its name.  Variables can become determined in the process of type 
checking, which is why you sometimes see types change from one query to 
another.  I believe this _is_ all covered in the Coq manual, though the 
details of printing type levels may not be.

> 4.  Is there a way of successfully querying (option_ind x) for some x? 
> The unset command doesn't appear to apply here.
>
> Coq < Unset Implicit Arguments.

This command only affects definitions yet to come.  You should use one 
of the notations for referencing identifiers with different implicitness 
behavior.  Either preface the identifier with [@] or use the 
[(argumentName := term)] notation.

As an alternate presentation of this material, I recommend Chapter 11 of 
CPDT (http://adam.chlipala.net/cpdt/).