Enter the interactive proof-builder

For proof-builder command summaries, see proof-builder.

Examples: (VERIFY (implies (and (true-listp x) (true-listp y)) (equal (append (append x y) z) (append x (append y z))))) -- Attempt to prove the given term interactively. (VERIFY (p x) :event-name p-always-holds :rule-classes (:rewrite :generalize) :instructions ((rewrite p-always-holds-lemma) change-goal)) -- Attempt to prove (p x), where the intention is to call the resulting DEFTHM event by the name p-always-holds, with rule-classes as indicated. The two indicated instructions will be run immediately to start the proof. (VERIFY) -- Re-enter the interactive proof-builder in the state at which it was most recently left. General Form: (VERIFY &OPTIONAL raw-term &KEY event-name rule-classes instructions)

Note that you can use

(verify (equal y y) :instructions (s (exit foo nil t)))

we can see that the expected event was successfully created:

ACL2 !>:pe foo 1:x(VERIFY (EQUAL Y Y) :INSTRUCTIONS ...) > (DEFTHM FOO (EQUAL Y Y) :RULE-CLASSES NIL :INSTRUCTIONS (:S)) ACL2 !>

That said, it's probably not a good idea to save events with