• 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

      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))))))