		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

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