coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Bounding the Type Hierarchy

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Bounding the Type Hierarchy
Date: Tue, 08 Dec 2015 15:59:39 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mailinglists AT robbertkrebbers.nl; spf=None smtp.mailfrom=mailinglists AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT smtp1.science.ru.nl
Ironport-phdr: 9a23:1TaNtRERwe9+KzGokq3yg51GYnF86YWxBRYc798ds5kLTJ75o8mwAkXT6L1XgUPTWs2DsrQf27SQ6/iocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC0YLvj6ibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0/MlZFK7+Yq4QTLpCDT1gPXpmytfssEz5SgGF62EAGkYMnxBCDhLepEX/V5b1sy31sutmxDKyJ8r8R70uRTe44q1hRQXzziEDYW1quFrLg9B92foI6CmqoAZyltbZ

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.

[Coq-Club] Bounding the Type Hierarchy, Dominique Larchey-Wendling, 12/08/2015
- Re: [Coq-Club] Bounding the Type Hierarchy, Robbert Krebbers, 12/08/2015
  - Re: [Coq-Club] Bounding the Type Hierarchy, Guillaume Melquiond, 12/08/2015
    - Re: [Coq-Club] Bounding the Type Hierarchy, Dominique Larchey-Wendling, 12/10/2015
      - Re: [Coq-Club] Bounding the Type Hierarchy, Guillaume Melquiond, 12/10/2015
- Re: [Coq-Club] Bounding the Type Hierarchy, Cedric Auger, 12/08/2015