		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printing-options

Irr-pprint-options

An irrelevant value of pretty-printing options.

Signature
(irr-pprint-options) → irr
Returns: irr — Type (pprint-options-p irr).

Definitions and Theorems

Function: irr-pprint-options

(defun irr-pprint-options nil
  (declare (xargs :guard t))
  (let ((__function__ 'irr-pprint-options))
    (declare (ignorable __function__))
    (make-pprint-options :parenthesize-nested-conditionals nil)))

Theorem: pprint-options-p-of-irr-pprint-options

(defthm pprint-options-p-of-irr-pprint-options
  (b* ((irr (irr-pprint-options)))
    (pprint-options-p irr))
  :rule-classes :rewrite)