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