		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.