		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))))))