general code completions #56

New issue

Open

opened 2026-10-16 14:10:53 +02:00 by EatOreo · 0 comments

EatOreo commented

2026-10-16 14:10:53 +02:00

Owner

when writing a crocq annotation you should get proposed the valid clauses as code completion (snippets preferably) based on what kind of annotation you are writing. For example in a function annotation suggest "PROOF ${1:file}:${1:proofName}".
Inside these we can in turn do even more completions, see #23.

https://code.visualstudio.com/api/language-extensions/programmatic-language-features#show-code-completion-proposals

when writing a crocq annotation you should get proposed the valid clauses as code completion (snippets preferably) based on what kind of annotation you are writing. For example in a function annotation suggest "PROOF ${1:file}:${1:proofName}". Inside these we can in turn do even more completions, see #23. https://code.visualstudio.com/api/language-extensions/programmatic-language-features#show-code-completion-proposals

EatOreo referenced this issue

2026-10-16 14:11:11 +02:00

code completions suggesting proofs/definitions to link to when writing a PROOF or SPEC clause #23