|
|
|---|
|
|
|
|---|
Get the kind (tag) of a command-error structure.
(command-error-kind x) → kind
Function:
(defun command-error-kind$inline (x) (declare (xargs :guard (command-error-p x))) (let ((__function__ 'command-error-kind)) (declare (ignorable __function__)) (mbe :logic (cond ((or (atom x) (eq (car x) :malformed-mnemonic)) :malformed-mnemonic) ((eq (car x) :malformed-passphrase) :malformed-passphrase) ((eq (car x) :malformed-entropy) :malformed-entropy) ((eq (car x) :malformed-nonce) :malformed-nonce) ((eq (car x) :malformed-gas-price) :malformed-gas-price) ((eq (car x) :malformed-gas-limit) :malformed-gas-limit) ((eq (car x) :malformed-to) :malformed-to) ((eq (car x) :malformed-value) :malformed-value) ((eq (car x) :malformed-data) :malformed-data) ((eq (car x) :malformed-address-key-index) :malformed-address-key-index) ((eq (car x) :address-key-index-too-large) :address-key-index-too-large) ((eq (car x) :address-key-index-skipped) :address-key-index-skipped) ((eq (car x) :root-key-derivation-fail) :root-key-derivation-fail) ((eq (car x) :purpose-key-derivation-fail) :purpose-key-derivation-fail) ((eq (car x) :coin-type-key-derivation-fail) :coin-type-key-derivation-fail) ((eq (car x) :account-key-derivation-fail) :account-key-derivation-fail) ((eq (car x) :external-chain-key-derivation-fail) :external-chain-key-derivation-fail) ((eq (car x) :address-key-derivation-fail) :address-key-derivation-fail) ((eq (car x) :address-key-index-limit) :address-key-index-limit) ((eq (car x) :pretransaction-rlp-fail) :pretransaction-rlp-fail) ((eq (car x) :transaction-sign-fail) :transaction-sign-fail) ((eq (car x) :transaction-rlp-fail) :transaction-rlp-fail) ((eq (car x) :state-file-untestable) :state-file-untestable) ((eq (car x) :state-file-absent) :state-file-absent) ((eq (car x) :state-file-present) :state-file-present) ((eq (car x) :state-file-not-regular) :state-file-not-regular) ((eq (car x) :state-file-malformed) :state-file-malformed) ((eq (car x) :wrong-number-of-arguments) :wrong-number-of-arguments) ((eq (car x) :wrong-command) :wrong-command) (t :no-command)) :exec (car x))))
Theorem:
(defthm command-error-kind-possibilities (or (equal (command-error-kind x) :malformed-mnemonic) (equal (command-error-kind x) :malformed-passphrase) (equal (command-error-kind x) :malformed-entropy) (equal (command-error-kind x) :malformed-nonce) (equal (command-error-kind x) :malformed-gas-price) (equal (command-error-kind x) :malformed-gas-limit) (equal (command-error-kind x) :malformed-to) (equal (command-error-kind x) :malformed-value) (equal (command-error-kind x) :malformed-data) (equal (command-error-kind x) :malformed-address-key-index) (equal (command-error-kind x) :address-key-index-too-large) (equal (command-error-kind x) :address-key-index-skipped) (equal (command-error-kind x) :root-key-derivation-fail) (equal (command-error-kind x) :purpose-key-derivation-fail) (equal (command-error-kind x) :coin-type-key-derivation-fail) (equal (command-error-kind x) :account-key-derivation-fail) (equal (command-error-kind x) :external-chain-key-derivation-fail) (equal (command-error-kind x) :address-key-derivation-fail) (equal (command-error-kind x) :address-key-index-limit) (equal (command-error-kind x) :pretransaction-rlp-fail) (equal (command-error-kind x) :transaction-sign-fail) (equal (command-error-kind x) :transaction-rlp-fail) (equal (command-error-kind x) :state-file-untestable) (equal (command-error-kind x) :state-file-absent) (equal (command-error-kind x) :state-file-present) (equal (command-error-kind x) :state-file-not-regular) (equal (command-error-kind x) :state-file-malformed) (equal (command-error-kind x) :wrong-number-of-arguments) (equal (command-error-kind x) :wrong-command) (equal (command-error-kind x) :no-command)) :rule-classes ((:forward-chaining :trigger-terms ((command-error-kind x)))))