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