		Search-engine friendly clone of the ACL2 documentation.

Printer

Init-pristate

Initial printer state.

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

We pass the printing options and the GCC flag, 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 gcc)
  (declare (xargs :guard (and (prioptp options) (booleanp gcc))))
  (let ((__function__ 'init-pristate))
    (declare (ignorable __function__))
    (make-pristate :bytes-rev nil
                   :indent-level 0
                   :options options
                   :gcc gcc)))

Theorem: pristatep-of-init-pristate

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

Theorem: pristate->gcc-of-init-pristate

(defthm pristate->gcc-of-init-pristate
  (b* ((?pstate (init-pristate options gcc)))
    (equal (pristate->gcc pstate)
           (bool-fix gcc))))

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

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

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 gcc)
                  (init-pristate options-equiv gcc)))
  :rule-classes :congruence)

Theorem: init-pristate-of-bool-fix-gcc

(defthm init-pristate-of-bool-fix-gcc
  (equal (init-pristate options (bool-fix gcc))
         (init-pristate options gcc)))

Theorem: init-pristate-iff-congruence-on-gcc

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