Guard-theorem
Use a previously-proved guard theorem
See lemma-instance for a discussion of :guard-theorem
lemma instances, as illustrated in the topic guard-theorem-example.
The function guard-theorem is a low-level system utility that returns
a translated term. It is essentially the functional version of the
gthm macro, which however returns an untranslated term. See gthm.
Subtopics
- ACL2-pc::prove-guard
- (macro)
Verify guards efficiently by using a previous guard theorem.
- Guard-theorem-example
- How to use a previously-proved guard theorem
