Print a universal character name.
(print-univ-char-name ucname pstate) → new-pstate
Function:
(defun print-univ-char-name (ucname pstate) (declare (xargs :guard (and (univ-char-name-p ucname) (pristatep pstate)))) (let ((__function__ 'print-univ-char-name)) (declare (ignorable __function__)) (univ-char-name-case ucname :locase-u (b* ((pstate (print-astring "\\u" pstate)) (pstate (print-hex-quad ucname.quad pstate))) pstate) :upcase-u (b* ((pstate (print-astring "\\U" pstate)) (pstate (print-hex-quad ucname.quad1 pstate)) (pstate (print-hex-quad ucname.quad2 pstate))) pstate))))
Theorem:
(defthm pristatep-of-print-univ-char-name (b* ((new-pstate (print-univ-char-name ucname pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-univ-char-name-of-univ-char-name-fix-ucname (equal (print-univ-char-name (univ-char-name-fix ucname) pstate) (print-univ-char-name ucname pstate)))
Theorem:
(defthm print-univ-char-name-univ-char-name-equiv-congruence-on-ucname (implies (univ-char-name-equiv ucname ucname-equiv) (equal (print-univ-char-name ucname pstate) (print-univ-char-name ucname-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-univ-char-name-of-pristate-fix-pstate (equal (print-univ-char-name ucname (pristate-fix pstate)) (print-univ-char-name ucname pstate)))
Theorem:
(defthm print-univ-char-name-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-univ-char-name ucname pstate) (print-univ-char-name ucname pstate-equiv))) :rule-classes :congruence)