• 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

    Make-honsed-strin

    Constructor macro for honsed strin-p structures.

    Syntax:

    (make-honsed-strin [:chars <chars>] 
                       [:line <line>] 
                       [:col <col>] 
                       [:file <file>]) 
    

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

    Definition

    This is an ordinary honsing make- macro introduced by defaggregate.

    Macro: make-honsed-strin

    (defmacro make-honsed-strin (&rest args)
      (std::make-aggregate 'strin
                           args '((:chars) (:line) (:col) (:file))
                           'make-honsed-strin
                           t))