Print a label.
Function:
(defun print-label (label pstate) (declare (xargs :guard (and (labelp label) (pristatep pstate)))) (let ((__function__ 'print-label)) (declare (ignorable __function__)) (label-case label :name (print-ident label.unwrap pstate) :const (b* ((pstate (print-astring "case " pstate)) (pstate (print-const-expr label.unwrap pstate))) pstate) :default (print-astring "default" pstate))))
Theorem:
(defthm pristatep-of-print-label (b* ((new-pstate (print-label label pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-label-of-label-fix-label (equal (print-label (label-fix label) pstate) (print-label label pstate)))
Theorem:
(defthm print-label-label-equiv-congruence-on-label (implies (label-equiv label label-equiv) (equal (print-label label pstate) (print-label label-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-label-of-pristate-fix-pstate (equal (print-label label (pristate-fix pstate)) (print-label label pstate)))
Theorem:
(defthm print-label-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-label label pstate) (print-label label pstate-equiv))) :rule-classes :congruence)