		Search-engine friendly clone of the ACL2 documentation.

String-codelist-conversions

Nats=>string

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

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

Definitions and Theorems

Function: nats=>string

(defun nats=>string (nats)
  (declare (xargs :guard (unsigned-byte-listp 8 nats)))
  (let ((__function__ 'nats=>string))
    (declare (ignorable __function__))
    (implode (nats=>chars nats))))

Theorem: stringp-of-nats=>string

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

Theorem: nth-of-explode-of-nats=>string

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

Theorem: len-of-explode-of-nats=>string

(defthm len-of-explode-of-nats=>string
  (equal (len (explode (nats=>string nats)))
         (len nats)))

Theorem: explode-of-nats=>string

(defthm explode-of-nats=>string
  (equal (explode (nats=>string nats))
         (nats=>chars nats)))

Subtopics

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