		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)))))