Stream: Coq users

Topic: Displaying universe constraints in proof

view this post on Zulip Jesse Reimann (Sep 14 2023 at 16:05):

I want to keep an eye on the universe constraints Coq imposes at different steps of a proof. Is there a more convenient way of doing this than adding Show Universes throughout the proof?

view this post on Zulip Gaëtan Gilbert (Sep 14 2023 at 16:06):

no

view this post on Zulip Ike Mulder (Sep 16 2023 at 15:50):

I find the universes subgraph command helpful, ie Print Universes Subgraph (prod.u0 list.u0). See also here

Last updated: Oct 13 2024 at 01:02 UTC