Increment a position by a number of lines.
The column is reset to 0.
Function:
(defun position-inc-line (lines pos) (declare (xargs :guard (and (posp lines) (positionp pos)))) (let ((__function__ 'position-inc-line)) (declare (ignorable __function__)) (make-position :line (+ (position->line pos) lines) :column 0)))
Theorem:
(defthm positionp-of-position-inc-line (b* ((new-pos (position-inc-line lines pos))) (positionp new-pos)) :rule-classes :rewrite)