		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-new-line

Print a new-line character.

Signature
(print-new-line pstate) → new-pstate
Arguments: pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

For now we print a single line feed character, which has code 10. In the future, we could support a printer option for the kind of new line character to use. Our parser supports (i) line feeds, (ii) carriage returns, and (iii) line feeds immediately followed by carriage returns.

Definitions and Theorems

Function: print-new-line

(defun print-new-line (pstate)
  (declare (xargs :guard (pristatep pstate)))
  (let ((__function__ 'print-new-line))
    (declare (ignorable __function__))
    (print-char 10 pstate)))

Theorem: pristatep-of-print-new-line

(defthm pristatep-of-print-new-line
  (b* ((new-pstate (print-new-line pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: print-new-line-of-pristate-fix-pstate

(defthm print-new-line-of-pristate-fix-pstate
  (equal (print-new-line (pristate-fix pstate))
         (print-new-line pstate)))

Theorem: print-new-line-pristate-equiv-congruence-on-pstate

(defthm print-new-line-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-new-line pstate)
                  (print-new-line pstate-equiv)))
  :rule-classes :congruence)