The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Thank you for your suggestion Guillaume.

> Print Sorted Universes "universes.txt".

Reading the generated file, I remark that there
are two kinds of informations:

1/ order constraints like Type.{n} < Type.{n+1}
2/ identity constraints like {path}.{number} = Type.{n}

I have some questions.

a/ what does the {number} mean ? An occurrence in the source code ?
b/ if Type.2 is the greatest Type.{n} that occurs in the list of
   constraints, can I deduce that all the loaded theorems can be
   proved in a restriction of the CIC with a Type hierarchy equal
   to
           Prop < Type.0 < Type.1 < Type.2

c/ After Cedric Auger's message, I am a bit confused. It seemed to
   me that CIC was equal to the limit \bigcup_n CIC(n) where
   CIC(n) is the restriction of the CIC where n bounds the highest
   level in the Type hierarchy. It seems (but may be I did not
   understand well) that Cedric suggests that CIC(n) might even
   be inconsistent ? In which case, the questions I am asking
   could be found odd.

Dominique

On 12/08/2015 05:04 PM, Guillaume Melquiond wrote:> On 08/12/2015 15:59,
Robbert Krebbers wrote:
>> On 12/08/2015 03:54 PM, Dominique Larchey-Wendling wrote:
>>> Another way to formulate the question is how can I know the maximum
>>> n such that Type_n is needed in the type-checking of a given proof ?
>> Maybe "Print Sorted Universes" will help. From the reference manual:
>>
>>   If the optional Sorted option is given, each universe will
>>   be made equivalent to a numbered label reflecting its level
>>   (with a linear ordering) in the universe hierarchy.
>
> Yes, that is the way to do it. For instance, Coq's testsuite executes
> the following script:
>
> Require all_stdlib.
> Print Sorted Universes "universes.txt".
>
> Then it parses the generated file to check that the number of universe
> levels needed to typecheck the standard library did not unexpectedly
change.
>
> Best regards,
>
> Guillaume
>