Stream: MetaCoq

Topic: Universes of term?


view this post on Zulip Jason Gross (Apr 24 2023 at 21:26):

Is there anything I can use to get all the universes (ContextSet.t) of a PCUICAst.term? (The safechecker is telling me "Sort contains an undeclared level")

view this post on Zulip Matthieu Sozeau (Apr 25 2023 at 09:11):

There is a universes_of_term function somewhere I think.

view this post on Zulip Matthieu Sozeau (Apr 25 2023 at 09:11):

Giving you a LevelSet.t

view this post on Zulip Jason Gross (Apr 25 2023 at 23:12):

git grep '\([Tt]erm[^ ]*[Uu]niv\|[Uu]niv[^ ]*[Tt]erm\)' gives only things matching eqb\?_term_upto_univ, maybe it's under a different name? (Indeed a LevelSet.t is what I want)

view this post on Zulip Matthieu Sozeau (Apr 26 2023 at 07:12):

Indeed, cannot find it anymore. I think at some point there was one in a plugin used to fix the declaration of universes but no longer


Last updated: Jul 23 2024 at 20:01 UTC