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