		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Charset-range

Signature
(charset-range x y) → chars
Arguments: x — Guard (characterp x).; y — Guard (characterp y).
Returns: chars — Type (character-listp chars).

Definitions and Theorems

Function: charset-range

(defun charset-range (x y)
  (declare (xargs :guard (and (characterp x) (characterp y))))
  (declare (xargs :guard (<= (char-code x) (char-code y))))
  (let ((__function__ 'charset-range))
    (declare (ignorable __function__))
    (b* ((x (mbe :logic (acl2::char-fix x) :exec x))
         ((when (mbe :logic (zp (- (char-code y) (char-code x)))
                     :exec (eql x y)))
          (list x))
         (next (code-char (+ 1 (char-code x)))))
      (cons x (charset-range next y)))))

Theorem: character-listp-of-charset-range

(defthm character-listp-of-charset-range
  (b* ((chars (charset-range x y)))
    (character-listp chars))
  :rule-classes :rewrite)

Theorem: charset-range-of-char-fix-x

(defthm charset-range-of-char-fix-x
  (equal (charset-range (acl2::char-fix x) y)
         (charset-range x y)))

Theorem: charset-range-chareqv-congruence-on-x

(defthm charset-range-chareqv-congruence-on-x
  (implies (acl2::chareqv x x-equiv)
           (equal (charset-range x y)
                  (charset-range x-equiv y)))
  :rule-classes :congruence)

Theorem: charset-range-of-char-fix-y

(defthm charset-range-of-char-fix-y
  (equal (charset-range x (acl2::char-fix y))
         (charset-range x y)))

Theorem: charset-range-chareqv-congruence-on-y

(defthm charset-range-chareqv-congruence-on-y
  (implies (acl2::chareqv y y-equiv)
           (equal (charset-range x y)
                  (charset-range x y-equiv)))
  :rule-classes :congruence)