		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-hex-digit-achar

Print an ACL2 hexadecimal digit character.

Signature
(print-hex-digit-achar achar pstate) → new-pstate
Arguments: achar — Guard (hex-digit-char-p achar).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

We turn the character into its code and print it. Note that we do not need the numeric value of the character; we just need to print the character itself.

This is essentially the same code as print-dec-digit-achar and print-oct-digit-achar, but it has a stronger guard than if we used a more general function to print an ACL2 character.

Definitions and Theorems

Function: print-hex-digit-achar

(defun print-hex-digit-achar (achar pstate)
  (declare (xargs :guard (and (hex-digit-char-p achar)
                              (pristatep pstate))))
  (let ((__function__ 'print-hex-digit-achar))
    (declare (ignorable __function__))
    (print-char (char-code achar) pstate)))

Theorem: pristatep-of-print-hex-digit-achar

(defthm pristatep-of-print-hex-digit-achar
  (b* ((new-pstate (print-hex-digit-achar achar pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: print-hex-digit-achar-of-pristate-fix-pstate

(defthm print-hex-digit-achar-of-pristate-fix-pstate
  (equal (print-hex-digit-achar achar (pristate-fix pstate))
         (print-hex-digit-achar achar pstate)))

Theorem: print-hex-digit-achar-pristate-equiv-congruence-on-pstate

(defthm print-hex-digit-achar-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-hex-digit-achar achar pstate)
                  (print-hex-digit-achar achar pstate-equiv)))
  :rule-classes :congruence)