		Search-engine friendly clone of the ACL2 documentation.

Pinst

Pinst-kind

Get the kind (tag) of a pinst structure.

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

Definitions and Theorems

Function: pinst-kind$inline

(defun pinst-kind$inline (x)
  (declare (xargs :guard (pinst-p x)))
  (let ((acl2::__function__ 'pinst-kind))
    (declare (ignorable acl2::__function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :flat)) :flat)
                      ((eq (car x) :keyline) :keyline)
                      ((eq (car x) :dot) :dot)
                      ((eq (car x) :quote) :quote)
                      ((eq (car x) :wide) :wide)
                      ((eq (car x) :keypair) :keypair)
                      ((eq (car x) :indent) :indent)
                      (t :special-term))
         :exec (car x))))

Theorem: pinst-kind-possibilities

(defthm pinst-kind-possibilities
  (or (equal (pinst-kind x) :flat)
      (equal (pinst-kind x) :keyline)
      (equal (pinst-kind x) :dot)
      (equal (pinst-kind x) :quote)
      (equal (pinst-kind x) :wide)
      (equal (pinst-kind x) :keypair)
      (equal (pinst-kind x) :indent)
      (equal (pinst-kind x) :special-term))
  :rule-classes
  ((:forward-chaining :trigger-terms ((pinst-kind x)))))