coq-lsp
coq-lsp copied to clipboard
ejgallego
Universe information
It is currently quite awkward to extract information about universes in Coq. During a proof, one typically has to resort to Show Universes to understand which universes are present. It might be useful to have a (minimized by default) window in the goals window to see the universe information. Essentially something that outputs Show Universes at each stage.
That seems like a good idea, why not?
Can you point out some proof that you would consider representative of your use case?
In HoTT we have Algebra/Rings/Matrix.v and typically after a rewrite there are many superfluous universe variables that get generated and then flattened at Defined.
That's interesting, maybe work reporting upstream?
Allow me some questions because I don't know this stuff very well, what's the typical workflow for this case?
- you do the rewrite
- you look at the universes
- then?