		Search-engine friendly clone of the ACL2 documentation.

Identifiers

Identifier-fix

Fixer for identifierp.

Signature
(identifier-fix x) → fixed-x
Arguments: x — Guard (identifierp x).
Returns: fixed-x — Type (identifierp fixed-x).

Definitions and Theorems

Function: identifier-fix

(defun identifier-fix (x)
  (declare (xargs :guard (identifierp x)))
  (mbe :logic
       (if (identifierp x)
           x
         (list (char-code #\$)))
       :exec x))

Theorem: identifierp-of-identifier-fix

(defthm identifierp-of-identifier-fix
  (b* ((fixed-x (identifier-fix x)))
    (identifierp fixed-x))
  :rule-classes :rewrite)

Theorem: identifier-fix-when-identifierp

(defthm identifier-fix-when-identifierp
  (implies (identifierp x)
           (equal (identifier-fix x) x)))