• 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-count-charset

Count how many characters at the start of the input stream are members of some particular character set.

Signature

(strin-count-charset set x) → *

Arguments

set — Guard (charset-p set).

x — Guard (strin-p x).

We just leave this enabled.

Definitions and Theorems

Function: strin-count-charset

(defun strin-count-charset (set x)
  (declare (xargs :guard (and (charset-p set) (strin-p x))))
  (let ((__function__ 'strin-count-charset))
    (declare (ignorable __function__))
    (count-leading-charset (strin-left x)
                           set)))