code2rocq/imp2rocq
Archived
Watch
3
0
Fork
You've already forked imp2rocq
 0
Code Issues 25 Pull requests Projects 2 Wiki Activity

Complete code lenses to jump to proofs #13

Open
opened 2026-03-12 15:19:33 +01:00 by marfavi · 0 comments
marfavi commented 2026-03-12 15:19:33 +01:00
Owner

Pre-postcondition contract's "Prove" code lens should jump to the *_correct theorem in the proof skeleton.

Loop invariants should have multiple code lenses to jump to the multiple proofs needed for loop invariants.

Pre-postcondition contract's "Prove" code lens should jump to the `*_correct` theorem in the proof skeleton. Loop invariants should have multiple code lenses to jump to the multiple proofs needed for loop invariants.
marfavi added this to the Kanban project 2026-03-12 15:19:36 +01:00
michael self-assigned this 2026-03-25 12:38:43 +01:00
Commenting is not possible because the repository is archived.
No Branch/Tag specified
Branches Tags
main
report
refactor-documents
parser
No results found.
Labels
Clear labels
No items
No labels
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Kanban
Assignees
Clear assignees
No assignees
michael
1 participant
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Depends on
#12 Generate "proof skeleton"
code2rocq/imp2rocq
#14 Keeping track of correlated pieces of code in annotations and generated Rocq files
code2rocq/imp2rocq
Reference
code2rocq/imp2rocq#13
No description provided.