• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Std/io
    • Oslib
    • Bridge
    • Clex
      • Example-lexer
      • Sin
        • Strin-p
          • Strin
          • Make-strin
          • Strin-left
          • Change-strin
          • Strin-get-file
          • Strin-get-col
          • Strin-nthcdr
          • Strin-get-line
          • Strin-cdr
          • Strin-find
          • Honsed-strin
          • Make-honsed-strin
          • Strin-matches-p
          • Strin-imatches-p
          • Strin-firstn
          • Strin-count-charset
          • Empty-strin
          • Strin-nth
          • Strin-len
          • Strin-endp
          • Strin-car
          • Strin->chars
          • Strin->line
          • Strin->col
          • Strin->file
        • Sin$c
      • Matching-functions
      • Def-sin-progress
    • Tshell
    • Unsound-eval
    • Hacker
    • ACL2s-interface
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Strin-p

Strin-get-line

Wrapper for strin->line that fixes the line number to a posp.

Signature

(strin-get-line x) → col

Arguments

x — Guard (strin-p x).

Returns

col — Type (posp col).

This just lets us always assume that sin-line is a posp. We typically just leave this disabled, because who wants to reason about line numbers?

Definitions and Theorems

Function: strin-get-line$inline

(defun strin-get-line$inline (x)
  (declare (xargs :guard (strin-p x)))
  (let ((__function__ 'strin-get-line))
    (declare (ignorable __function__))
    (mbe :logic
         (let ((line (strin->line x)))
           (if (posp line) line 1))
         :exec (strin->line x))))

Theorem: posp-of-strin-get-line

(defthm posp-of-strin-get-line
  (b* ((col (strin-get-line$inline x)))
    (posp col))
  :rule-classes :type-prescription)