• 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

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