• 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

    Raw constructor for strin-p structures.

    Syntax:

    (strin chars line col file)

    This is the lowest-level constructor for strin-p structures. It simply conses together a structure with the specified fields.

    Note: It's generally better to use macros like make-strin or change-strin instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.

    The strin-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-strin instead.

    Definition

    This is an ordinary constructor function introduced by defaggregate.

    Function: strin

    (defun strin (chars line col file)
      (declare (xargs :guard (and (character-listp chars)
                                  (posp line)
                                  (natp col)
                                  (stringp file))))
      (cons :strin (cons (cons 'chars chars)
                         (cons (cons 'line line)
                               (cons (cons 'col col)
                                     (cons (cons 'file file) nil))))))