Get the kind (tag) of a vl-slicesize structure.
(vl-slicesize-kind x) → kind
Function:
(defun vl-slicesize-kind$inline (x) (declare (xargs :guard (vl-slicesize-p x))) (let ((__function__ 'vl-slicesize-kind)) (declare (ignorable __function__)) (mbe :logic (cond ((eq (car x) :expr) :expr) ((eq (car x) :type) :type) (t :none)) :exec (car x))))
Theorem:
(defthm vl-slicesize-kind-possibilities (or (equal (vl-slicesize-kind x) :expr) (equal (vl-slicesize-kind x) :type) (equal (vl-slicesize-kind x) :none)) :rule-classes ((:forward-chaining :trigger-terms ((vl-slicesize-kind x)))))