Increase the printer state's indentation level by one.
Function:
(defun inc-pristate-indent (pstate) (declare (xargs :guard (pristatep pstate))) (let ((__function__ 'inc-pristate-indent)) (declare (ignorable __function__)) (change-pristate pstate :indent-level (1+ (pristate->indent-level pstate)))))
Theorem:
(defthm pristatep-of-inc-pristate-indent (b* ((new-pstate (inc-pristate-indent pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm inc-pristate-indent-of-pristate-fix-pstate (equal (inc-pristate-indent (pristate-fix pstate)) (inc-pristate-indent pstate)))
Theorem:
(defthm inc-pristate-indent-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (inc-pristate-indent pstate) (inc-pristate-indent pstate-equiv))) :rule-classes :congruence)