code2rocq/crocq
code2rocq/crocq
Watch
3
2
Fork
You've already forked crocq
 0
Code Issues 18 Pull requests 3 Projects 1 Releases 1 Packages 2 Activity Actions

interpret proof codelens #49

New issue
Closed
opened 2026-10-16 11:04:12 +02:00 by EatOreo · 0 comments
EatOreo commented 2026-10-16 11:04:12 +02:00
Owner

code lens above proof clauses that opens the document in another pane and runs the interpret to point command to the end of the proof.

code lens above proof clauses that opens the document in another pane and runs the interpret to point command to the end of the proof.
EatOreo self-assigned this 2026-10-16 11:04:14 +02:00
Sign in to join this conversation.
No Branch/Tag specified
Branches Tags
main
release/0.1.0
fix/resync-on-v-rename
feat/infer-inline-declare
feat/grammar-highlighting
feat/clightgen-command-in-status
fix/code-lens-annotation-top
feature/proof-status
fix/inline-clauses-review-findings
v0.1.0
Labels
Clear labels   
blocked
should wait for another issue to be addressed

  
bug

   
priority!

   
quick-pick
No labels
blocked
bug
priority!
quick-pick
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
EatOreo
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference
code2rocq/crocq#49
No description provided.