		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-line-blank

Pretty-print a blank line of code.

Signature
(pprint-line-blank) → line
Returns: line — Type (msgp line).

Definitions and Theorems

Function: pprint-line-blank

(defun pprint-line-blank nil
  (declare (xargs :guard t))
  (let ((__function__ 'pprint-line-blank))
    (declare (ignorable __function__))
    "~%"))

Theorem: msgp-of-pprint-line-blank

(defthm msgp-of-pprint-line-blank
  (b* ((line (pprint-line-blank)))
    (msgp line))
  :rule-classes :rewrite)