		Search-engine friendly clone of the ACL2 documentation.

Grammar-printer-implementation

Pretty-print-rule

Pretty-print a rule.

Signature
(pretty-print-rule rule) → string
Arguments: rule — Guard (rulep rule).
Returns: string — Type (common-lisp::stringp string).

Definitions and Theorems

Function: pretty-print-rule

(defun pretty-print-rule (rule)
  (declare (xargs :guard (rulep rule)))
  (let ((__function__ 'pretty-print-rule))
    (declare (ignorable __function__))
    (b* (((rule rule) rule))
      (str::cat (rulename->get rule.name)
                (if rule.incremental "=/" "=")
                (pretty-print-alternation rule.definiens)))))

Theorem: stringp-of-pretty-print-rule

(defthm stringp-of-pretty-print-rule
  (b* ((string (pretty-print-rule rule)))
    (common-lisp::stringp string))
  :rule-classes :rewrite)