Decrease the printer state's indentation level by one.
We ensure that the current indentation level is not 0, throwing a hard error if that happens (which would make the level negative when decremented). This is an internal error: it should never happen, but if it may happen if there is a bug in our printer.
Function:
(defun dec-pristate-indent (pstate) (declare (xargs :guard (pristatep pstate))) (let ((__function__ 'dec-pristate-indent)) (declare (ignorable __function__)) (b* ((indent-level (pristate->indent-level pstate)) ((when (= indent-level 0)) (raise "Internal error: ~ attempting to decrease a zero indentation level.") (pristate-fix pstate))) (change-pristate pstate :indent-level (1- indent-level)))))
Theorem:
(defthm pristatep-of-dec-pristate-indent (b* ((new-pstate (dec-pristate-indent pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm dec-pristate-indent-of-pristate-fix-pstate (equal (dec-pristate-indent (pristate-fix pstate)) (dec-pristate-indent pstate)))
Theorem:
(defthm dec-pristate-indent-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (dec-pristate-indent pstate) (dec-pristate-indent pstate-equiv))) :rule-classes :congruence)