coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Find all universes in a term

From: Jason Gross <jasongross9 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 04:02:06 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f180.google.com
Ironport-phdr: 9a23:AAaUZBVI8SXGS/jxB5M1Xs1hbDjV8LGtZVwlr6E/grcLSJyIuqrYZhSDt8tkgFKBZ4jH8fUM07OQ6PG6HzFRqsnR+DBaKdoXCE9D0Z1X1yUbQ+e7SmTDZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5yO/inUtWK15f//6mI9pbSewRFgiamKfM3dU3u7FaZis5Dqox7Yo011xGB9nBPYqFdwX5iDVOVhRf1oMmqqs1N6SNV7tAo7MlGGYrgeL8jBehaBS8hNW8v49bw5DHMSAKO4j0XVWBAwUkAOBTM8ByvBsS5iSD9rOconXDCZcA=

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.30
MirrorCore.EnvI.30 <= Coq.Init.Datatypes.51
Urefl <= 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

[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