		Search-engine friendly clone of the ACL2 documentation.

Using-computed-hints

Using-computed-hints-1

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