		Search-engine friendly clone of the ACL2 documentation.

Symbol-fix

(symbol-fix x) is a fixing function for symbolp; it is the identity for symbols and coerces non-symbols to acl2::||, i.e., the empty symbol in the ACL2 package.

Unfortunately it's not currently possible to come up with a good symbol-fixing function that induces the proper congruences for both symbol-name and symbol-package-name. This definition at least gives us a congruence for symbol-name.

BOZO consider adding a symbolp guard, inlining it, and turning it into an identity function for execution.

Definitions and Theorems

Function: symbol-fix

(defun symbol-fix (x)
  (declare (xargs :guard t))
  (if (symbolp x) x '||))

Theorem: symbolp-of-symbol-fix

(defthm symbolp-of-symbol-fix
  (symbolp (symbol-fix x))
  :rule-classes :type-prescription)

Theorem: symbol-fix-when-symbolp

(defthm symbol-fix-when-symbolp
  (implies (symbolp x)
           (equal (symbol-fix x) x)))