Driving Home the Basics
The common hint
("Subgoal 3.2.1''" :use lemma42)
has the same effect as the computed hint
(if (equal id '((0) (3 2 1) . 2)) '(:use lemma42) nil)
which, of course, is equivalent to
(and (equal id '((0) (3 2 1) . 2)) '(:use lemma42))
which is also equivalent to the computed hint
my-special-hint
provided the following
(defun my-special-hint (id clause world) (declare (xargs :mode :program) (ignore clause world)) (if (equal id '((0) (3 2 1) . 2)) '(:use lemma42) nil))
It is permitted for the
Just to be concrete, the following three events all behave the same way (if
(defthm main (big-thm a b c) :hints (("Subgoal 3.2.1''" :use lemma42))) (defthm main (big-thm a b c) :hints ((and (equal id '((0) (3 2 1) . 2)) '(:use lemma42)))) (defthm main (big-thm a b c) :hints (my-special-hint))