		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-nice-bytes

Human-friendly summary of some number of bytes.

Signature
(vl-nice-bytes bytes) → str
Arguments: bytes — Guard (natp bytes).
Returns: str — Type (stringp str).

Definitions and Theorems

Function: vl-nice-bytes

(defun vl-nice-bytes (bytes)
  (declare (xargs :guard (natp bytes)))
  (let ((__function__ 'vl-nice-bytes))
    (declare (ignorable __function__))
    (b* (((when (< bytes 1000))
          (cat (natstr bytes) "B"))
         (kbytes (truncate bytes 1000))
         ((when (< kbytes 1000))
          (cat (natstr kbytes)
               "."
               (natstr (truncate (rem bytes 1000) 100))
               "K"))
         (mbytes (truncate kbytes 1000))
         ((when (< mbytes 1000))
          (cat (natstr mbytes)
               "."
               (natstr (truncate (rem kbytes 1000) 100))
               "M"))
         (gbytes (truncate mbytes 1000)))
      (cat (natstr gbytes)
           "."
           (natstr (truncate (rem mbytes 1000) 100))
           "G"))))

Theorem: stringp-of-vl-nice-bytes

(defthm stringp-of-vl-nice-bytes
  (b* ((str (vl-nice-bytes bytes)))
    (stringp str))
  :rule-classes :type-prescription)