		Search-engine friendly clone of the ACL2 documentation.

Rlp-error

Rlp-error-kind

Get the kind (tag) of a rlp-error structure.

Signature
(rlp-error-kind x) → kind
Arguments: x — Guard (rlp-error-p x).

Definitions and Theorems

Function: rlp-error-kind$inline

(defun rlp-error-kind$inline (x)
  (declare (xargs :guard (rlp-error-p x)))
  (let ((__function__ 'rlp-error-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :no-bytes))
                       :no-bytes)
                      ((eq (car x)
                           :fewer-bytes-than-short-length)
                       :fewer-bytes-than-short-length)
                      ((eq (car x)
                           :fewer-bytes-than-length-of-length)
                       :fewer-bytes-than-length-of-length)
                      ((eq (car x)
                           :fewer-bytes-than-long-length)
                       :fewer-bytes-than-long-length)
                      ((eq (car x)
                           :leading-zeros-in-long-length)
                       :leading-zeros-in-long-length)
                      ((eq (car x) :non-optimal-short-length)
                       :non-optimal-short-length)
                      ((eq (car x) :non-optimal-long-length)
                       :non-optimal-long-length)
                      ((eq (car x) :subtree) :subtree)
                      ((eq (car x) :extra-bytes) :extra-bytes)
                      ((eq (car x) :branch-tree) :branch-tree)
                      (t :leading-zeros-in-scalar))
         :exec (car x))))

Theorem: rlp-error-kind-possibilities

(defthm rlp-error-kind-possibilities
  (or (equal (rlp-error-kind x) :no-bytes)
      (equal (rlp-error-kind x)
             :fewer-bytes-than-short-length)
      (equal (rlp-error-kind x)
             :fewer-bytes-than-length-of-length)
      (equal (rlp-error-kind x)
             :fewer-bytes-than-long-length)
      (equal (rlp-error-kind x)
             :leading-zeros-in-long-length)
      (equal (rlp-error-kind x)
             :non-optimal-short-length)
      (equal (rlp-error-kind x)
             :non-optimal-long-length)
      (equal (rlp-error-kind x) :subtree)
      (equal (rlp-error-kind x) :extra-bytes)
      (equal (rlp-error-kind x) :branch-tree)
      (equal (rlp-error-kind x)
             :leading-zeros-in-scalar))
  :rule-classes
  ((:forward-chaining :trigger-terms ((rlp-error-kind x)))))