		Search-engine friendly clone of the ACL2 documentation.

Character-literals

Unicode-charlit-char-fix

Fixer for unicode-charlit-char.

Signature
(unicode-charlit-char-fix x) → fixed-x
Arguments: x — Guard (unicode-charlit-char-p x).
Returns: fixed-x — Type (unicode-charlit-char-p fixed-x).

Definitions and Theorems

Function: unicode-charlit-char-fix

(defun unicode-charlit-char-fix (x)
  (declare (xargs :guard (unicode-charlit-char-p x)))
  (mbe :logic
       (if (unicode-charlit-char-p x)
           x
         (make-unicode-input-char :unicode 0
                                  :umarker 0))
       :exec x))

Theorem: unicode-charlit-char-p-of-unicode-charlit-char-fix

(defthm unicode-charlit-char-p-of-unicode-charlit-char-fix
  (b* ((fixed-x (unicode-charlit-char-fix x)))
    (unicode-charlit-char-p fixed-x))
  :rule-classes :rewrite)

Theorem: unicode-charlit-char-fix-when-unicode-charlit-char-p

(defthm unicode-charlit-char-fix-when-unicode-charlit-char-p
  (implies (unicode-charlit-char-p x)
           (equal (unicode-charlit-char-fix x) x)))