Represent a position as a message.
This is used in user-oriented error messages.
Function:
(defun position-to-msg (pos) (declare (xargs :guard (positionp pos))) (let ((__function__ 'position-to-msg)) (declare (ignorable __function__)) (msg "(line ~x0, column ~x1)" (position->line pos) (position->column pos))))
Theorem:
(defthm msgp-of-position-to-msg (b* ((msg (position-to-msg pos))) (msgp msg)) :rule-classes :rewrite)