The formula of a name or rune

The ACL2 system function,

When ACL2 is given a

(formula x t wrld) ; for :use hints (formula x nil wrld) ; for :by hints

The second argument can affect whether or not to use a normalized version
of the term (in particular, a definition body) associated with

Here are some examples. Note that

(defun f1 (x) (cons 3 x)) (defun f2 (x y) (implies x y)) (defthm one-rule (and (equal (* 2 y) (+ y y)) (equal (* 3 y) (+ y y y)))) (defthm two-rules t :rule-classes ((:rewrite :corollary (equal (* 2 y) (+ y y))) (:rewrite :corollary (equal (* 3 y) (+ y y y)))))

Then:

ACL2 !>(formula 'f1 nil (w state)) (EQUAL (F1 X) (CONS '3 X)) ACL2 !>(formula 'f1 t (w state)) (EQUAL (F1 X) (CONS '3 X)) ACL2 !>(formula 'f2 nil (w state)) (EQUAL (F2 X Y) (IMPLIES X Y)) ACL2 !>(formula 'f2 t (w state)) (EQUAL (F2 X Y) (IF X (IF Y 'T 'NIL) 'T)) ACL2 !>(formula 'one-rule nil (w state)) (IF (EQUAL (BINARY-* '2 Y) (BINARY-+ Y Y)) (EQUAL (BINARY-* '3 Y) (BINARY-+ Y (BINARY-+ Y Y))) 'NIL) ACL2 !>(equal (formula 'one-rule nil (w state)) (formula 'one-rule t (w state))) T ACL2 !>(formula 'two-rules nil (w state)) 'T ACL2 !>(formula 'two-rules t (w state)) 'T ACL2 !>(formula '(:rewrite two-rules . 1) nil (w state)) (EQUAL (BINARY-* '2 Y) (BINARY-+ Y Y)) ACL2 !>(formula '(:rewrite two-rules . 2) nil (w state)) (EQUAL (BINARY-* '3 Y) (BINARY-+ Y (BINARY-+ Y Y))) ACL2 !>(formula 'no-such-rule nil (w state)) NIL ACL2 !>