		Search-engine friendly clone of the ACL2 documentation.

Hprefix

Hprefix-kind

Get the kind (tag) of a hprefix structure.

Signature
(hprefix-kind x) → kind
Arguments: x — Guard (hprefixp x).

Definitions and Theorems

Function: hprefix-kind$inline

(defun hprefix-kind$inline (x)
  (declare (xargs :guard (hprefixp x)))
  (let ((__function__ 'hprefix-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :locase-0x))
                       :locase-0x)
                      (t :upcase-0x))
         :exec (car x))))

Theorem: hprefix-kind-possibilities

(defthm hprefix-kind-possibilities
  (or (equal (hprefix-kind x) :locase-0x)
      (equal (hprefix-kind x) :upcase-0x))
  :rule-classes
  ((:forward-chaining :trigger-terms ((hprefix-kind x)))))