		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jline-blank

Pretty-print a blank line of code.

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

Definitions and Theorems

Function: print-jline-blank

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

Theorem: msgp-of-print-jline-blank

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