• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
      • Pretty-printing
      • Printtree
      • Base64
      • Charset-p
      • Strtok!
      • Cases
      • Concatenation
      • Html-encoding
      • Character-kinds
      • Substrings
      • Strtok
      • Equivalences
      • Url-encoding
      • Lines
        • Strlines
        • Prefix-lines
        • Strline
      • Ordering
      • Numbers
      • Pad-trim
      • Coercion
      • Std/strings-extensions
      • Std/strings/digit-to-char
      • Substitution
      • Symbols
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Lines

Strline

Extract a line from a string by its line number.

(strline n x) extracts the nth line from the string x and returns it as a string. The string will not contain a newline character.

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 require n to be a posp.

If n does not refer to a valid line number for x, the empty string is returned.

Definitions and Theorems

Function: strline

(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)))))

Theorem: stringp-of-strline

(defthm stringp-of-strline
        (stringp (strline n x))
        :rule-classes :type-prescription)