Get the kind (tag) of a bitsize structure.
(bitsize-kind x) → kind
Function:
(defun bitsize-kind$inline (x) (declare (xargs :guard (bitsizep x))) (let ((__function__ 'bitsize-kind)) (declare (ignorable __function__)) (mbe :logic (cond ((or (atom x) (eq (car x) :|8|)) :|8|) ((eq (car x) :|16|) :|16|) ((eq (car x) :|32|) :|32|) ((eq (car x) :|64|) :|64|) (t :|128|)) :exec (car x))))
Theorem:
(defthm bitsize-kind-possibilities (or (equal (bitsize-kind x) :|8|) (equal (bitsize-kind x) :|16|) (equal (bitsize-kind x) :|32|) (equal (bitsize-kind x) :|64|) (equal (bitsize-kind x) :|128|)) :rule-classes ((:forward-chaining :trigger-terms ((bitsize-kind x)))))