Get the kind (tag) of a dec/oct/hex-const structure.
(dec/oct/hex-const-kind x) → kind
Function:
(defun dec/oct/hex-const-kind$inline (x) (declare (xargs :guard (dec/oct/hex-constp x))) (let ((__function__ 'dec/oct/hex-const-kind)) (declare (ignorable __function__)) (mbe :logic (cond ((or (atom x) (eq (car x) :dec)) :dec) ((eq (car x) :oct) :oct) (t :hex)) :exec (car x))))
Theorem:
(defthm dec/oct/hex-const-kind-possibilities (or (equal (dec/oct/hex-const-kind x) :dec) (equal (dec/oct/hex-const-kind x) :oct) (equal (dec/oct/hex-const-kind x) :hex)) :rule-classes ((:forward-chaining :trigger-terms ((dec/oct/hex-const-kind x)))))