		Search-engine friendly clone of the ACL2 documentation.

Signed-format

Signed-format-kind

Get the kind (tag) of a signed-format structure.

Signature
(signed-format-kind x) → kind
Arguments: x — Guard (signed-formatp x).

Definitions and Theorems

Function: signed-format-kind$inline

(defun signed-format-kind$inline (x)
  (declare (xargs :guard (signed-formatp x)))
  (let ((__function__ 'signed-format-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x)
                           (eq (car x) :sign-magnitude))
                       :sign-magnitude)
                      ((eq (car x) :ones-complement)
                       :ones-complement)
                      (t :twos-complement))
         :exec (car x))))

Theorem: signed-format-kind-possibilities

(defthm signed-format-kind-possibilities
  (or (equal (signed-format-kind x)
             :sign-magnitude)
      (equal (signed-format-kind x)
             :ones-complement)
      (equal (signed-format-kind x)
             :twos-complement))
  :rule-classes
  ((:forward-chaining :trigger-terms ((signed-format-kind x)))))