		Search-engine friendly clone of the ACL2 documentation.

Typecode

Code->ctype

Get the combinational-type keyword from its numeric encoding.

Signature
(code->ctype x) → ctype
Arguments: x — Guard (typecodep x).
Returns: ctype — Type (ctypep ctype).

Definitions and Theorems

Function: code->ctype

(defun code->ctype (x)
       (declare (xargs :guard (typecodep x)))
       (let ((__function__ 'code->ctype))
            (declare (ignorable __function__))
            (car (rassoc (typecode-fix x)
                         *ctype-code-map*))))

Theorem: ctypep-of-code->ctype

(defthm ctypep-of-code->ctype
        (b* ((ctype (code->ctype x)))
            (ctypep ctype))
        :rule-classes :rewrite)

Theorem: code->ctype-of-typecode

(defthm code->ctype-of-typecode
        (equal (code->ctype (typecode x))
               (ctype-fix x)))

Theorem: typecode-of-code->ctype

(defthm typecode-of-code->ctype
        (equal (typecode (code->ctype x))
               (typecode-fix x)))

Theorem: normalize-typecode-equivalence

(defthm normalize-typecode-equivalence
        (equal (equal (typecode x) code)
               (and (typecodep code)
                    (equal (ctype-fix x)
                           (code->ctype code)))))