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

Peek at the first character in the input stream.

Signature

(strin-car x) → *

Arguments

x — Guard (strin-p x).

We just leave this enabled.

Definitions and Theorems

Function: strin-car

(defun strin-car (x)
  (declare (xargs :guard (strin-p x)))
  (let ((__function__ 'strin-car))
    (declare (ignorable __function__))
    (car (strin-left x))))