		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)