Increment a position by a number of columns.
The line number is unchanged.
Function:
(defun position-inc-column (columns pos) (declare (xargs :guard (and (natp columns) (positionp pos)))) (let ((__function__ 'position-inc-column)) (declare (ignorable __function__)) (change-position pos :column (+ (position->column pos) columns))))
Theorem:
(defthm positionp-of-position-inc-column (b* ((new-pos (position-inc-column columns pos))) (positionp new-pos)) :rule-classes :rewrite)