• 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-col

Wrapper for strin->col that fixes the column number to a natp.

Signature

(strin-get-col x) → col

Arguments

x — Guard (strin-p x).

Returns

col — Type (natp col).

This just lets us always assume that sin-col is a natural. We typically just leave this disabled, because who wants to reason about column number? (Well, maybe for Python you need something like that...)

Definitions and Theorems

Function: strin-get-col$inline

(defun strin-get-col$inline (x)
  (declare (xargs :guard (strin-p x)))
  (let ((__function__ 'strin-get-col))
    (declare (ignorable __function__))
    (lnfix (strin->col x))))

Theorem: natp-of-strin-get-col

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