		Search-engine friendly clone of the ACL2 documentation.

Node

Stype

Get the kind (tag) of a node structure.

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

Definitions and Theorems

Function: stype$inline

(defun stype$inline (x)
  (declare (xargs :guard (node-p x)))
  (let ((__function__ 'stype))
    (declare (ignorable __function__))
    (mbe :logic
         (cond ((or (atom x)
                    (not (stypep (car x)))
                    (eq (car x) :const))
                :const)
               ((eq (car x) :pi) :pi)
               ((eq (car x) :reg) :reg)
               ((eq (car x) :and) :and)
               ((eq (car x) :xor) :xor)
               ((eq (car x) :po) :po)
               ((eq (car x) :nxst) :nxst))
         :exec
         (if (atom x)
             :const
           (stype-fix (car x))))))

Theorem: stype-possibilities

(defthm stype-possibilities
  (or (equal (stype x) :const)
      (equal (stype x) :pi)
      (equal (stype x) :reg)
      (equal (stype x) :and)
      (equal (stype x) :xor)
      (equal (stype x) :po)
      (equal (stype x) :nxst))
  :rule-classes ((:forward-chaining :trigger-terms ((stype x)))))

Theorem: stypep-of-stype

(defthm stypep-of-stype
  (stypep (stype x)))

Theorem: stype-not-const-implies-nonempty

(defthm stype-not-const-implies-nonempty
  (implies (not (equal (stype (car x)) (const-stype)))
           (consp x))
  :rule-classes
  ((:forward-chaining :trigger-terms ((stype (car x))))))