Extract a line from a string by its line number.
(strline n x) extracts the
Note that we consider the first line of the string to be 1, not 0. This is
intended to agree with the convention followed by many text editors, where the
first line in a file is regarded as line 1 instead of line 0. Accordingly, we
(defun strline (n x) (declare (xargs :guard (and (posp n) (stringp x)))) (let* ((x (mbe :logic (if (stringp x) x "") :exec x)) (xl (length x)) (start (go-to-line x 0 xl 1 n))) (if (not start) "" (let ((end (charpos-aux x start xl #\Newline))) (subseq x start end)))))
(defthm stringp-of-strline (stringp (strline n x)) :rule-classes :type-prescription)