Pretty-print a list of rules.
(pretty-print-rulelist rules) → string
Function:
(defun pretty-print-rulelist (rules) (declare (xargs :guard (rulelistp rules))) (let ((__function__ 'pretty-print-rulelist)) (declare (ignorable __function__)) (cond ((endp rules) "") ((endp (cdr rules)) (str::cat (pretty-print-rule (car rules)) (implode (list (code-char 13) (code-char 10))))) (t (str::cat (pretty-print-rule (car rules)) (implode (list (code-char 13) (code-char 10))) (pretty-print-rulelist (cdr rules)))))))
Theorem:
(defthm stringp-of-pretty-print-rulelist (b* ((string (pretty-print-rulelist rules))) (common-lisp::stringp string)) :rule-classes :rewrite)