The Coq mailing list

[Jeffrey Terrell <jeff AT kc.com>]

Hi,

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 *)?

Coq < Set Printing Universes.

Coq < Check Set.
Set
     : Type (* (0)+1 *)

Coq < Check Type.
Type (* Top.1 *)
     : Type (* (Top.1)+1 *)

Coq < Check Type (* (Top.1)+1 *).
Type (* Top.2 *)
     : Type (* (Top.2)+1 *)

2.  Why does the type of Type change from one query to another?

Coq < Check Type.
Type (* Top.1 *)
     : Type (* (Top.1)+1 *)

Coq < Check Type.
Type (* Top.2 *)
     : Type (* (Top.2)+1 *)

Coq < Check Type.
Type (* Top.3 *)
     : Type (* (Top.3)+1 *)

3.  What is the type of Type in option_ind?

Coq < Check option_ind.
option_ind
     : forall (A : Type (* Coq.Init.Datatypes.20 *)) (P : option A -> Prop),
       (forall a : A, P (Some a)) -> P None -> forall o : option A, P o

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.

Coq < Check (option_ind Type).
Toplevel input, characters 18-22:
> Check (option_ind Type).
>                   ^^^^
Error: The term "Type (* Top.9 *)" has type "Type (* (Top.9)+1 *)"
 while it is expected to have type "option ?6 -> Prop".

Thanks.

Regards,
Jeff.