		Search-engine friendly clone of the ACL2 documentation.

Representation

Typecode

Numeric encoding of a combinational-type keyword.

Signature
(typecode x) → code
Arguments: x — Guard (ctypep x).
Returns: code — Type (natp code).

Definitions and Theorems

Function: typecode

(defun typecode (x)
       (declare (xargs :guard (ctypep x)))
       (let ((__function__ 'typecode))
            (declare (ignorable __function__))
            (cdr (assoc (ctype-fix x)
                        *ctype-code-map*))))

Theorem: natp-of-typecode

(defthm natp-of-typecode
        (b* ((code (typecode x))) (natp code))
        :rule-classes (:rewrite :type-prescription))

Theorem: typecode-bound

(defthm typecode-bound (< (typecode x) 4)
        :rule-classes :linear)

Theorem: typecodep-of-typecode

(defthm typecodep-of-typecode
        (typecodep (typecode x)))

Subtopics

Code->ctype: Get the combinational-type keyword from its numeric encoding.
Node->type: Get the combinational typecode from a logical node.
Typecode-fix: Fixing function for typecodes.
Typecodep: Recognizer for valid typecodes.
*ctype-code-map*