• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • 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
  • 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-imatches-p

See if some string literal occurs (case insensitively) at the start of the input stream.

Signature

(strin-imatches-p lit x) → *

Arguments

lit — Guard (stringp lit).

x — Guard (strin-p x).

We just leave this enabled.

Definitions and Theorems

Function: strin-imatches-p

(defun strin-imatches-p (lit x)
  (declare (xargs :guard (and (stringp lit) (strin-p x))))
  (let ((__function__ 'strin-imatches-p))
    (declare (ignorable __function__))
    (str::iprefixp (coerce lit 'list)
                   (strin-left x))))