		Search-engine friendly clone of the ACL2 documentation.

Lhatom

Lhatom-kind

Get the kind (tag) of a lhatom structure.

Signature
(lhatom-kind x) → kind
Arguments: x — Guard (lhatom-p x).

Definitions and Theorems

Function: lhatom-kind$inline

(defun lhatom-kind$inline (x)
  (declare (xargs :guard (lhatom-p x)))
  (let ((__function__ 'lhatom-kind))
    (declare (ignorable __function__))
    (cond ((eq x :z) :z) (t :var))))

Theorem: lhatom-kind-possibilities

(defthm lhatom-kind-possibilities
  (or (equal (lhatom-kind x) :z)
      (equal (lhatom-kind x) :var))
  :rule-classes
  ((:forward-chaining :trigger-terms ((lhatom-kind x)))))