		Search-engine friendly clone of the ACL2 documentation.

Printer

Init-pristate

Initial printer state.

Signature
(init-pristate options) → pstate
Arguments: options — Guard (prioptp options).
Returns: pstate — Type (pristatep pstate).

We pass the printing options, which must be provided externally.

Initially, no data has been printed, and the indentation level is 0.

Definitions and Theorems

Function: init-pristate

(defun init-pristate (options)
  (declare (xargs :guard (prioptp options)))
  (let ((__function__ 'init-pristate))
    (declare (ignorable __function__))
    (make-pristate :bytes-rev nil
                   :indent-level 0
                   :options options)))

Theorem: pristatep-of-init-pristate

(defthm pristatep-of-init-pristate
  (b* ((pstate (init-pristate options)))
    (pristatep pstate))
  :rule-classes :rewrite)

Theorem: init-pristate-of-priopt-fix-options

(defthm init-pristate-of-priopt-fix-options
  (equal (init-pristate (priopt-fix options))
         (init-pristate options)))

Theorem: init-pristate-priopt-equiv-congruence-on-options

(defthm init-pristate-priopt-equiv-congruence-on-options
  (implies (priopt-equiv options options-equiv)
           (equal (init-pristate options)
                  (init-pristate options-equiv)))
  :rule-classes :congruence)