search

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
135 stars 31 forks source link

Universe information #797

Open Alizter opened 1 week ago

Alizter commented 1 week ago

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.

ejgallego commented 1 week ago

That seems like a good idea, why not?

Can you point out some proof that you would consider representative of your use case?

Alizter commented 1 week ago

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.

ejgallego commented 1 week ago

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?

  1. you do the rewrite
  2. you look at the universes
  3. then?