Generate "proof skeleton" #12

Open

opened 2026-03-12 15:16:22 +01:00 by marfavi · 0 comments

marfavi commented

2026-03-12 15:16:22 +01:00

Owner

From precondition and postcondition, create a *_correct/*_pre_and_postconditions_hold theorem to be proved
From loop invariants, create a loop invariant definition & relevant theorems.
Use both the *_correct and loop invariant definition for compile checking the contracts (hook to vsrocqtop)
Show squiggles in the correct places in the contracts on compilation error

* From precondition and postcondition, create a `*_correct`/`*_pre_and_postconditions_hold` theorem to be proved * From loop invariants, create a loop invariant definition & relevant theorems. * Use both the `*_correct` and loop invariant definition for compile checking the contracts (hook to `vsrocqtop`) * Show squiggles in the correct places in the contracts on compilation error

marfavi added this to the Kanban project

2026-03-12 15:16:22 +01:00

marfavi added a new dependency

2026-03-12 15:19:52 +01:00

#13 Complete code lenses to jump to proofs

marfavi self-assigned this

2026-03-12 15:20:22 +01:00

Commenting is not possible because the repository is archived.