Print a declaration, in its own indented line.
Function:
(defun print-decl (decl pstate) (declare (xargs :guard (and (declp decl) (pristatep pstate)))) (declare (xargs :guard (decl-unambp decl))) (let ((__function__ 'print-decl)) (declare (ignorable __function__)) (b* ((pstate (print-indent pstate)) (pstate (print-decl-inline decl pstate)) (pstate (print-new-line pstate))) pstate)))
Theorem:
(defthm pristatep-of-print-decl (b* ((new-pstate (print-decl decl pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-decl-of-decl-fix-decl (equal (print-decl (decl-fix decl) pstate) (print-decl decl pstate)))
Theorem:
(defthm print-decl-decl-equiv-congruence-on-decl (implies (decl-equiv decl decl-equiv) (equal (print-decl decl pstate) (print-decl decl-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-decl-of-pristate-fix-pstate (equal (print-decl decl (pristate-fix pstate)) (print-decl decl pstate)))
Theorem:
(defthm print-decl-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-decl decl pstate) (print-decl decl pstate-equiv))) :rule-classes :congruence)