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