Initial printer state.
We pass the size of the indentation, because that is an option that must be provided externally.
Initially, no data has been printed, and the indentation level is 0.
Function:
(defun init-pristate (indent-size) (declare (xargs :guard (posp indent-size))) (let ((__function__ 'init-pristate)) (declare (ignorable __function__)) (make-pristate :bytes-rev nil :indent-level 0 :indent-size indent-size)))
Theorem:
(defthm pristatep-of-init-pristate (b* ((pstate (init-pristate indent-size))) (pristatep pstate)) :rule-classes :rewrite)