		Search-engine friendly clone of the ACL2 documentation.
Opcode
Opcode-p

Recognizer for opcode structures.
Signature
(opcode-p x) → *
Definitions and Theorems

Function: opcode-p
(defun opcode-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'opcode-p))
  (declare (ignorable __function__))
  (and
    (std::prod-consp x)
    (std::prod-consp (std::prod-car x))
    (std::prod-consp (std::prod-car (std::prod-car x)))
    (std::prod-consp
         (std::prod-cdr (std::prod-car (std::prod-car x))))
    (std::prod-consp (std::prod-cdr (std::prod-car x)))
    (std::prod-consp
         (std::prod-cdr (std::prod-cdr (std::prod-car x))))
    (std::prod-consp (std::prod-cdr x))
    (std::prod-consp (std::prod-car (std::prod-cdr x)))
    (std::prod-consp
         (std::prod-cdr (std::prod-car (std::prod-cdr x))))
    (std::prod-consp (std::prod-cdr (std::prod-cdr x)))
    (std::prod-consp
         (std::prod-cdr (std::prod-cdr (std::prod-cdr x))))
    (b*
     ((op (std::prod-car (std::prod-car (std::prod-car x))))
      (mode (std::prod-car
                 (std::prod-cdr (std::prod-car (std::prod-car x)))))
      (reg (std::prod-cdr
                (std::prod-cdr (std::prod-car (std::prod-car x)))))
      (mod (std::prod-car (std::prod-cdr (std::prod-car x))))
      (r/m (std::prod-car
                (std::prod-cdr (std::prod-cdr (std::prod-car x)))))
      (pfx (std::prod-cdr
                (std::prod-cdr (std::prod-cdr (std::prod-car x)))))
      (rex (std::prod-car (std::prod-car (std::prod-cdr x))))
      (vex (std::prod-car
                (std::prod-cdr (std::prod-car (std::prod-cdr x)))))
      (evex (std::prod-cdr
                 (std::prod-cdr (std::prod-car (std::prod-cdr x)))))
      (feat (std::prod-car (std::prod-cdr (std::prod-cdr x))))
      (superscripts
           (std::prod-car
                (std::prod-cdr (std::prod-cdr (std::prod-cdr x)))))
      (group
           (std::prod-cdr
                (std::prod-cdr (std::prod-cdr (std::prod-cdr x))))))
     (and (24bits-p op)
          (op-mode-p mode)
          (maybe-3bits-p reg)
          (mod-p mod)
          (maybe-3bits-p r/m)
          (op-pfx-p pfx)
          (rex-p rex)
          (maybe-vex-p vex)
          (maybe-evex-p evex)
          (symbol-listp feat)
          (superscripts-p superscripts)
          (opcode-extension-group-p group))))))