Wrong hover descriptions on constants

[tirix]

In general, the correct description is provided when hovering over constants:

However, in some cases, there is a shift between the correct description and the description shown:

Here, the correct description for /\ would be: Wedge (read: 'and')
But the description shown is: Vee (read: 'or')

[tirix]

The reason is that metamath-knife expects the comment for a given statement just before that statement, as it is systematically the case for all axioms and theorems. However in the case of many constant declarations (but not all), it is provided just after them.

Obviously there is a more general question here, about whether we shall have a strict formatting for comments associated to $c constant declarations, or implement a kind of empirical rule (like, "if a comment follows on the same line, it is the associated comment").

I don't expect this issue to be fixed quickly, and there will probably no change to be done on the Visual Studio Code extension or LSP server, but I wanted to track it anyway since it will probably raise questions.