		Search-engine friendly clone of the ACL2 documentation.

Node->type

Get the combinational typecode from a logical node.

Signature
(node->type node) → typecode
Arguments: node — Guard (node-p node).
Returns: typecode — Type (natp typecode).

Definitions and Theorems

Function: node->type

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

Theorem: natp-of-node->type

(defthm natp-of-node->type
        (b* ((typecode (node->type node)))
            (natp typecode))
        :rule-classes :type-prescription)

Theorem: node->type-of-node-fix-node

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

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

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