		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-hex-const

Pretty-print a hexadecimal constant.

Signature
(pprint-hex-const n) → part
Arguments: n — Guard (natp n).
Returns: part — Type (msgp part).

According to the grammar [C:6.4.4.1], a `hexadecimal constant' is a sequence of hexadecimal digits preceded by 0x or 0X; with the optional suffixes, this becomes an integer constant. We print this with lowercase prefix and with no leading zeros, unless the number is 0, in which case we print 0x0.

Definitions and Theorems

Function: pprint-hex-const

(defun pprint-hex-const (n)
  (declare (xargs :guard (natp n)))
  (let ((__function__ 'pprint-hex-const))
    (declare (ignorable __function__))
    (str::cat "0x"
              (str::nat-to-hex-string (lnfix n)))))

Theorem: msgp-of-pprint-hex-const

(defthm msgp-of-pprint-hex-const
  (b* ((part (pprint-hex-const n)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-hex-const-of-nfix-n

(defthm pprint-hex-const-of-nfix-n
  (equal (pprint-hex-const (nfix n))
         (pprint-hex-const n)))

Theorem: pprint-hex-const-nat-equiv-congruence-on-n

(defthm pprint-hex-const-nat-equiv-congruence-on-n
  (implies (acl2::nat-equiv n n-equiv)
           (equal (pprint-hex-const n)
                  (pprint-hex-const n-equiv)))
  :rule-classes :congruence)