		Search-engine friendly clone of the ACL2 documentation.

Identifiers

Midentifier-fix

Fixer for midentifierp.

Signature
(midentifier-fix x) → fixed-x
Arguments: x — Guard (midentifierp x).
Returns: fixed-x — Type (midentifierp fixed-x).

Definitions and Theorems

Function: midentifier-fix

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

Theorem: midentifierp-of-midentifier-fix

(defthm midentifierp-of-midentifier-fix
  (b* ((fixed-x (midentifier-fix x)))
    (midentifierp fixed-x))
  :rule-classes :rewrite)

Theorem: midentifier-fix-when-midentifierp

(defthm midentifier-fix-when-midentifierp
  (implies (midentifierp x)
           (equal (midentifier-fix x) x)))