		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)