		Search-engine friendly clone of the ACL2 documentation.

Identifiers

Umidentifier-fix

Fixer for umidentifierp.

Signature
(umidentifier-fix x) → fixed-x
Arguments: x — Guard (umidentifierp x).
Returns: fixed-x — Type (umidentifierp fixed-x).

Definitions and Theorems

Function: umidentifier-fix

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

Theorem: umidentifierp-of-umidentifier-fix

(defthm umidentifierp-of-umidentifier-fix
  (b* ((fixed-x (umidentifier-fix x)))
    (umidentifierp fixed-x))
  :rule-classes :rewrite)

Theorem: umidentifier-fix-when-umidentifierp

(defthm umidentifier-fix-when-umidentifierp
  (implies (umidentifierp x)
           (equal (umidentifier-fix x) x)))