		Search-engine friendly clone of the ACL2 documentation.

Inst

Inst-p

Recognizer for inst structures.

Signature
(inst-p x) → *

Definitions and Theorems

Function: inst-p

(defun inst-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'inst-p))
  (declare (ignorable __function__))
  (and
     (std::prod-consp x)
     (std::prod-consp (std::prod-car x))
     (std::prod-consp (std::prod-cdr x))
     (std::prod-consp (std::prod-cdr (std::prod-cdr x)))
     (b* ((mnemonic (std::prod-car (std::prod-car x)))
          (opcode (std::prod-cdr (std::prod-car x)))
          (operands (std::prod-car (std::prod-cdr x)))
          (fn (std::prod-car (std::prod-cdr (std::prod-cdr x))))
          (excep (std::prod-cdr (std::prod-cdr (std::prod-cdr x)))))
       (and (mnemonic-p mnemonic)
            (strict-opcode-p opcode)
            (maybe-operands-p operands)
            (fn-desc-p fn)
            (exception-desc-p excep))))))