Pretty-print a prose value notation.
(pretty-print-prose-val proseval) → string
Function:
(defun pretty-print-prose-val (proseval) (declare (xargs :guard (prose-val-p proseval))) (let ((__function__ 'pretty-print-prose-val)) (declare (ignorable __function__)) (str::cat "<" (prose-val->get proseval) ">")))
Theorem:
(defthm stringp-of-pretty-print-prose-val (b* ((string (pretty-print-prose-val proseval))) (common-lisp::stringp string)) :rule-classes :rewrite)