		Search-engine friendly clone of the ACL2 documentation.

Command-error

Command-error-p

Recognizer for command-error structures.

Signature
(command-error-p x) → *

Definitions and Theorems

Function: command-error-p

(defun command-error-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'command-error-p))
  (declare (ignorable __function__))
  (and (consp x)
       (cond ((or (atom x)
                  (eq (car x) :malformed-mnemonic))
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 1)
                   (b* ((mnemonic (std::da-nth 0 (cdr x))))
                     (stringp mnemonic))))
             ((eq (car x) :malformed-passphrase)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 1)
                   (b* ((passphrase (std::da-nth 0 (cdr x))))
                     (stringp passphrase))))
             ((eq (car x) :malformed-entropy)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 1)
                   (b* ((entropy (std::da-nth 0 (cdr x))))
                     (stringp entropy))))
             ((eq (car x) :malformed-nonce)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 1)
                   (b* ((nonce (std::da-nth 0 (cdr x))))
                     (stringp nonce))))
             ((eq (car x) :malformed-gas-price)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 1)
                   (b* ((gas-price (std::da-nth 0 (cdr x))))
                     (stringp gas-price))))
             ((eq (car x) :malformed-gas-limit)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 1)
                   (b* ((gas-limit (std::da-nth 0 (cdr x))))
                     (stringp gas-limit))))
             ((eq (car x) :malformed-to)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 1)
                   (b* ((to (std::da-nth 0 (cdr x))))
                     (stringp to))))
             ((eq (car x) :malformed-value)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 1)
                   (b* ((value (std::da-nth 0 (cdr x))))
                     (stringp value))))
             ((eq (car x) :malformed-data)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 1)
                   (b* ((data (std::da-nth 0 (cdr x))))
                     (stringp data))))
             ((eq (car x)
                  :malformed-address-key-index)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 1)
                   (b* ((address-key-index (std::da-nth 0 (cdr x))))
                     (stringp address-key-index))))
             ((eq (car x)
                  :address-key-index-too-large)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 2)
                   (b* ((address-key-index (std::da-nth 0 (cdr x)))
                        (limit (std::da-nth 1 (cdr x))))
                     (and (natp address-key-index)
                          (natp limit)))))
             ((eq (car x) :address-key-index-skipped)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 1)
                   (b* ((address-key-index (std::da-nth 0 (cdr x))))
                     (natp address-key-index))))
             ((eq (car x) :root-key-derivation-fail)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 0)
                   (b* nil t)))
             ((eq (car x)
                  :purpose-key-derivation-fail)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 0)
                   (b* nil t)))
             ((eq (car x)
                  :coin-type-key-derivation-fail)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 0)
                   (b* nil t)))
             ((eq (car x)
                  :account-key-derivation-fail)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 0)
                   (b* nil t)))
             ((eq (car x)
                  :external-chain-key-derivation-fail)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 0)
                   (b* nil t)))
             ((eq (car x)
                  :address-key-derivation-fail)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 1)
                   (b* ((address-key-index (std::da-nth 0 (cdr x))))
                     (natp address-key-index))))
             ((eq (car x) :address-key-index-limit)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 0)
                   (b* nil t)))
             ((eq (car x) :pretransaction-rlp-fail)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 0)
                   (b* nil t)))
             ((eq (car x) :transaction-sign-fail)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 0)
                   (b* nil t)))
             ((eq (car x) :transaction-rlp-fail)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 0)
                   (b* nil t)))
             ((eq (car x) :state-file-untestable)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 0)
                   (b* nil t)))
             ((eq (car x) :state-file-absent)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 0)
                   (b* nil t)))
             ((eq (car x) :state-file-present)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 0)
                   (b* nil t)))
             ((eq (car x) :state-file-not-regular)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 0)
                   (b* nil t)))
             ((eq (car x) :state-file-malformed)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 0)
                   (b* nil t)))
             ((eq (car x) :wrong-number-of-arguments)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 2)
                   (b* ((required (std::da-nth 0 (cdr x)))
                        (given (std::da-nth 1 (cdr x))))
                     (and (natp required) (natp given)))))
             ((eq (car x) :wrong-command)
              (and (true-listp (cdr x))
                   (eql (len (cdr x)) 1)
                   (b* ((command (std::da-nth 0 (cdr x))))
                     (stringp command))))
             (t (and (eq (car x) :no-command)
                     (and (true-listp (cdr x))
                          (eql (len (cdr x)) 0))
                     (b* nil t)))))))

Theorem: consp-when-command-error-p

(defthm consp-when-command-error-p
  (implies (command-error-p x) (consp x))
  :rule-classes :compound-recognizer)