USING-COMPUTED-HINTS-1

Driving Home the Basics 
Major Section:  MISCELLANEOUS

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 has first been executed 
(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 defun to be in :LOGIC mode (see defun-mode) also.

Just to be concrete, the following three events all behave the same way (if my-special-hint is as above):

(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))