		Search-engine friendly clone of the ACL2 documentation.

Operand-type-p

Signature
(operand-type-p x) → *

Definitions and Theorems

Function: operand-type-p

(defun operand-type-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'operand-type-p))
    (declare (ignorable __function__))
    (or (not x)
        (acl2::keyword-listp x)
        (and (true-listp x)
             (if (equal (len x) 1)
                 (or (acl2-numberp (nth 0 x))
                     (addressing-method-code-p (nth 0 x)))
               (if (equal (len x) 2)
                   (and (addressing-method-code-p (nth 0 x))
                        (operand-type-code-p (nth 1 x)))
                 nil))))))

Function: operand-type-fix

(defun operand-type-fix (x)
  (declare (xargs :guard (operand-type-p x)))
  (let ((__function__ 'operand-type-fix))
    (declare (ignorable __function__))
    (mbe :logic (if (operand-type-p x) x 'nil)
         :exec x)))

Function: operand-type-equiv$inline

(defun operand-type-equiv$inline (x y)
  (declare (xargs :guard (and (operand-type-p x)
                              (operand-type-p y))))
  (equal (operand-type-fix x)
         (operand-type-fix y)))

Theorem: operand-type-equiv-is-an-equivalence

(defthm operand-type-equiv-is-an-equivalence
  (and (booleanp (operand-type-equiv x y))
       (operand-type-equiv x x)
       (implies (operand-type-equiv x y)
                (operand-type-equiv y x))
       (implies (and (operand-type-equiv x y)
                     (operand-type-equiv y z))
                (operand-type-equiv x z)))
  :rule-classes (:equivalence))

Theorem: operand-type-equiv-implies-equal-operand-type-fix-1

(defthm operand-type-equiv-implies-equal-operand-type-fix-1
  (implies (operand-type-equiv x x-equiv)
           (equal (operand-type-fix x)
                  (operand-type-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: operand-type-fix-under-operand-type-equiv

(defthm operand-type-fix-under-operand-type-equiv
  (operand-type-equiv (operand-type-fix x)
                      x)
  :rule-classes (:rewrite :rewrite-quoted-constant))