Code suggestions - Githubissues

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq

GNU Lesser General Public License v2.1

152 stars 32 forks source link

Open ejgallego opened 2 years ago

ejgallego commented 2 years ago

In order to try the repair code feature, we can suggest users two hints for Qed / Admitted proofs:

when the proof is broken, suggest the user to use Admitted.
when a proof that is not broken ends in Admitted, suggest switching it to Qed.

Whether having Admitted upstream is a good thing, I don't know.

ejgallego commented 2 years ago

This is more a showcase for the LSP feature than a useful thing, as our error recovery will insert admitted on Qed , so I dunno.

ejgallego commented 1 year ago

Another interesting one is to suggest the user to add proof terminators to proofs that are closed by a tactic.