coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gregory Malecha <gmalecha AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Find all universes in a term
- Date: Fri, 21 Oct 2016 14:18:15 +0000
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gmalecha AT gmail.com; spf=Pass smtp.mailfrom=gmalecha AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f169.google.com
- Ironport-phdr: 9a23:KlqaIxDOFdguVU8DfxT/UyQJP3N1i/DPJgcQr6AfoPdwSP79o8bcNUDSrc9gkEXOFd2CrakV0ayI6+u/AyQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd+IyZrvnL/os7ToICxwzAKnZr1zKBjk5S7wjeIxxbVYF6Aq1xHSqWFJcekFjUlhJFaUggqurpzopM0r221qtvkg789NV7nhN+R9FOQATWduD2dgz8ry/TLHUAHHsnAbSyAdlgdCKwnD9hDzGJnr5HjUrO14jQaAMMLxV6F8fD2m4qxrQVe8hyIOMzMy8Gj/hcl5jaYdqxWk8U8si7XIaZ2YYaItNpjWeskXEC8YBp5c
I see. Thanks.
On Fri, Oct 21, 2016 at 4:21 AM Matthieu Sozeau <mattam AT mattam.org> wrote:
In this particular case you should look what Coq.Init.Datatypes.51 corresponds to, probably some inductive parameter, and see to what the inductive is applied in your term.On Fri, Oct 21, 2016 at 6:02 AM Jason Gross <jasongross9 AT gmail.com> wrote:Note that reduction can leave over floating universes
Definition foo := Eval hnf in let T := Type in let enforce := (Type : (Type : T)) in T.
Perhaps it comes from that, or from tactics?On Thu, Oct 20, 2016, 11:48 PM Gregory Malecha <gmalecha AT gmail.com> wrote:Hello --Is there a way to get Coq to tell you where a universe comes from in a term? I know that you can do:Set Printing All.Set Printing Universes.and then say:Print foo.To see all of the universe annotations, but this is giving me odd output for a particular function. In particular, the universe annotation is:(* MirrorCore.EnvI.30 |= Set <= MirrorCore.EnvI.30MirrorCore.EnvI.30 <= Coq.Init.Datatypes.51Urefl <= MirrorCore.EnvI.30*)But when I search the text of the term, MirrorCore.EnvI.30 does not occur anywhere.Any pointers would be greatly appreciated.--- gregory malecha
gmalecha.github.io
--
- gregory malecha
gmalecha.github.io
- [Coq-Club] Find all universes in a term, Gregory Malecha, 10/21/2016
- Re: [Coq-Club] Find all universes in a term, Jason Gross, 10/21/2016
- Re: [Coq-Club] Find all universes in a term, Matthieu Sozeau, 10/21/2016
- Re: [Coq-Club] Find all universes in a term, Gregory Malecha, 10/21/2016
- Re: [Coq-Club] Find all universes in a term, Matthieu Sozeau, 10/21/2016
- Re: [Coq-Club] Find all universes in a term, Jason Gross, 10/21/2016
Archive powered by MHonArc 2.6.18.