code actions for annotation clauses with diagnostics #67

New issue

Open

opened 2026-10-22 09:50:42 +02:00 by EatOreo · 0 comments

EatOreo commented

2026-10-22 09:50:42 +02:00

Owner

we are doing something like this already for the stale model check in extension/src/language_features/crocqCodeAction.ts.
when we apply diagnostics to clauses we could also provide some actions to fix them with cmd+.,
consider:
PROOF filename:proofname
If file "filename" is not found: does it end with ".v"? else suggest a quick fix adding it. Else suggest generating the skeleton file for it.
If "filename" exists but "proofname" does not: suggest generating the theorem scaffold and putting it inside the file.

we are doing something like this already for the stale model check in extension/src/language_features/crocqCodeAction.ts. when we apply diagnostics to clauses we could also provide some actions to fix them with cmd+., consider: `PROOF filename:proofname` If file "filename" is not found: does it end with ".v"? else suggest a quick fix adding it. Else suggest generating the skeleton file for it. If "filename" exists but "proofname" does not: suggest generating the theorem scaffold and putting it inside the file.