		Search-engine friendly clone of the ACL2 documentation.

Node

Node->regp

Get the regp/xorp bit of a node's encoding -- 1 if it is a :reg, :nxst, or :xor node. Note: returns a bitp.

Signature
(node->regp node) → bit
Arguments: node — Guard (node-p node).
Returns: bit — Type (bitp bit).

Definitions and Theorems

Function: node->regp

(defun node->regp (node)
       (declare (xargs :guard (node-p node)))
       (let ((__function__ 'node->regp))
            (declare (ignorable __function__))
            (regp (stype node))))

Theorem: bitp-of-node->regp

(defthm bitp-of-node->regp
        (b* ((bit (node->regp node)))
            (bitp bit))
        :rule-classes :rewrite)

Theorem: node->regp-of-node-fix-node

(defthm node->regp-of-node-fix-node
        (equal (node->regp (node-fix node))
               (node->regp node)))

Theorem: node->regp-node-equiv-congruence-on-node

(defthm node->regp-node-equiv-congruence-on-node
        (implies (node-equiv node node-equiv)
                 (equal (node->regp node)
                        (node->regp node-equiv)))
        :rule-classes :congruence)