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):


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: Jun 23 2024 at 04:03 UTC