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