		Search-engine friendly clone of the ACL2 documentation.

String-codelist-conversions

String=>nats

Convert a string to the corresponding true list of natural numbers below 256.

Signature
(string=>nats string) → nats
Arguments: string — Guard (stringp string).
Returns: nats — Type (unsigned-byte-listp 8 nats).

Definitions and Theorems

Function: string=>nats

(defun string=>nats (string)
       (declare (xargs :guard (stringp string)))
       (let ((__function__ 'string=>nats))
            (declare (ignorable __function__))
            (chars=>nats (explode string))))

Theorem: return-type-of-string=>nats

(defthm return-type-of-string=>nats
        (b* ((nats (string=>nats string)))
            (unsigned-byte-listp 8 nats))
        :rule-classes :rewrite)

Theorem: nat-listp-of-string=>nats

(defthm nat-listp-of-string=>nats
        (b* ((nats (string=>nats string)))
            (nat-listp nats))
        :rule-classes :rewrite)

Theorem: len-of-string=>nats

(defthm len-of-string=>nats
        (implies (stringp string)
                 (equal (len (string=>nats string))
                        (length string))))

Theorem: nth-of-string=>nats

(defthm nth-of-string=>nats
        (equal (nth n (string=>nats string))
               (if (< (nfix n) (len (explode string)))
                   (char-code (char string n))
                   nil)))

Theorem: consp-of-string=>nats

(defthm consp-of-string=>nats
        (iff (consp (string=>nats string))
             (consp (explode string))))

Theorem: string=>nats-of-implode

(defthm string=>nats-of-implode
        (implies (character-listp chars)
                 (equal (string=>nats (implode chars))
                        (chars=>nats chars))))

Theorem: string=>nats-of-str-fix-string

(defthm string=>nats-of-str-fix-string
        (equal (string=>nats (str-fix string))
               (string=>nats string)))

Theorem: string=>nats-streqv-congruence-on-string

(defthm string=>nats-streqv-congruence-on-string
        (implies (streqv string string-equiv)
                 (equal (string=>nats string)
                        (string=>nats string-equiv)))
        :rule-classes :congruence)

Subtopics

Nats<=>string-inverses-theorems: nats=>string and string=>nats are mutual inverses.