		Search-engine friendly clone of the ACL2 documentation.

Pad-trim

Trim-bag

Remove particular characters from the front and end of a string.

(trim-bag x bag) removes the characters in bag from the front and end of the string x.

BOZO eventually make this efficient.

Definitions and Theorems

Function: trim-aux

(defun trim-aux (x bag)
       (declare (xargs :guard (and (character-listp x)
                                   (character-listp bag))))
       (if (consp x)
           (if (member (car x) bag)
               (trim-aux (cdr x) bag)
               x)
           nil))

Theorem: character-listp-of-trim-aux

(defthm character-listp-of-trim-aux
        (implies (force (character-listp x))
                 (character-listp (trim-aux x bag))))

Function: trim-bag

(defun trim-bag (x bag)
       (declare (xargs :guard (and (stringp x)
                                   (character-listp bag))))
       (let* ((chars (explode x))
              (chars (trim-aux chars bag))
              (chars (reverse chars))
              (chars (trim-aux chars bag))
              (chars (reverse chars)))
             (implode chars)))

Theorem: stringp-of-trim-bag

(defthm stringp-of-trim-bag
        (stringp (trim-bag x bag))
        :rule-classes :type-prescription)