Represent a span as a message.
This is used in user-oriented messages.
Function:
(defun span-to-msg (span) (declare (xargs :guard (spanp span))) (let ((__function__ 'span-to-msg)) (declare (ignorable __function__)) (msg "[~@0 to ~@1]" (position-to-msg (span->start span)) (position-to-msg (span->end span)))))
Theorem:
(defthm msgp-of-span-to-msg (b* ((msg (span-to-msg span))) (msgp msg)) :rule-classes :rewrite)