search

ejgallego / coq-lsp

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

hovering over record types should display the record #564

Open Alizter opened 1 year ago

Alizter commented 1 year ago

Currently our hover function only shows the type. This can be pretty useless when hovering over Inductive and Record types as it will just report Type. We should make it also print the definitions in those cases.

This is probably a nicer user experience.

ejgallego commented 1 year ago

I agree, also cc #341

ejgallego commented 1 year ago

I've just merged #562 which adds extensible hover support, this could be fixed by writing an OCaml function from Ast.t to the required markdown.