		Search-engine friendly clone of the ACL2 documentation.

Label

Label-kind

Get the kind (tag) of a label structure.

Signature
(label-kind x) → kind
Arguments: x — Guard (labelp x).

Definitions and Theorems

Function: label-kind$inline

(defun label-kind$inline (x)
  (declare (xargs :guard (labelp x)))
  (let ((__function__ 'label-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :name)) :name)
                      ((eq (car x) :cas) :cas)
                      (t :default))
         :exec (car x))))

Theorem: label-kind-possibilities

(defthm label-kind-possibilities
  (or (equal (label-kind x) :name)
      (equal (label-kind x) :cas)
      (equal (label-kind x) :default))
  :rule-classes
  ((:forward-chaining :trigger-terms ((label-kind x)))))