		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-oct-const

Pretty-print an octal constant.

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

According to the grammar [C:6.4.4.1], an `octal constant' is a sequence of octal digits starting with 0; with the optional suffixes, this becomes an integer constant.

Definitions and Theorems

Function: pprint-oct-const

(defun pprint-oct-const (n)
  (declare (xargs :guard (natp n)))
  (let ((__function__ 'pprint-oct-const))
    (declare (ignorable __function__))
    (if (zp n)
        "0"
      (str::cat "0" (str::nat-to-oct-string n)))))

Theorem: msgp-of-pprint-oct-const

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

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

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

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

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