• 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

Honsed-strin

Raw constructor for honsed strin-p structures.

Syntax:

(honsed-strin chars line col file)

This is identical to strin, except that we hons the structure we are creating.

Definition

This is an ordinary honsing constructor introduced by defaggregate.

Function: honsed-strin

(defun honsed-strin (chars line col file)
 (declare (xargs :guard (and (character-listp chars)
                             (posp line)
                             (natp col)
                             (stringp file))))
 (mbe
   :logic (strin chars line col file)
   :exec
   (hons :strin (hons (hons 'chars chars)
                      (hons (hons 'line line)
                            (hons (hons 'col col)
                                  (hons (hons 'file file) nil)))))))