		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Preproc-legible

Signature
(preproc-legible x) → new-x
Arguments: x — Guard (stringp x).
Returns: new-x — Type (stringp new-x).

Definitions and Theorems

Function: preproc-legible

(defun preproc-legible (x)
  (declare (xargs :guard (stringp x)))
  (let ((__function__ 'preproc-legible))
    (declare (ignorable __function__))
    (preproc-legible-aux x 0 nil)))

Theorem: stringp-of-preproc-legible

(defthm stringp-of-preproc-legible
  (b* ((new-x (preproc-legible x)))
    (stringp new-x))
  :rule-classes :type-prescription)

Theorem: preproc-legible-of-str-fix-x

(defthm preproc-legible-of-str-fix-x
  (equal (preproc-legible (acl2::str-fix x))
         (preproc-legible x)))

Theorem: preproc-legible-streqv-congruence-on-x

(defthm preproc-legible-streqv-congruence-on-x
  (implies (acl2::streqv x x-equiv)
           (equal (preproc-legible x)
                  (preproc-legible x-equiv)))
  :rule-classes :congruence)