Is Theorem keyword a synonym for Lemma in PVerifier? #933
Answered
by
AD1024
dasblinkenlight
asked this question in
Q&A
|
PVerifier's documentation talks about lemmas, but examples mention both Lemma and Theorem keywords in a similar context. From the parser source code it appears that the two keywords can be used interchangeably. Is it so, or is there a difference? |
Answered by
AD1024
Feb 8, 2026
Replies: 1 comment
|
Hi @dasblinkenlight |
0 replies
Answer selected by
dasblinkenlight
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Hi @dasblinkenlight
Yes,
LemmaandTheoremcan be used interchangeably (without affecting the generated verification conditions). They are mainly for the developers to distinguish between the main goals (usually safety properties) and auxiliary inductive invariants that finishes the proof.