• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • 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
          • Fmt
          • Msg
          • Cw
          • Set-evisc-tuple
          • Set-iprint
          • Print-control
          • Read-file-into-string
          • Std/io
          • Msgp
            • Printing-to-strings
            • Evisc-tuple
            • Output-controls
            • Observation
            • *standard-co*
            • Ppr-special-syms
            • Standard-oi
            • Standard-co
            • Without-evisc
            • Serialize
            • Output-to-file
            • Fmt-to-comment-window
            • Princ$
            • Character-encoding
            • Open-output-channel!
            • Cw-print-base-radix
            • Set-print-case
            • Set-print-base
            • Print-object$
            • Extend-pathname
            • Print-object$+
            • Fmx-cw
            • Set-print-radix
            • Set-fmt-hard-right-margin
            • File-write-date$
            • Proofs-co
            • Set-print-base-radix
            • Print-base-p
            • *standard-oi*
            • Wof
            • File-length$
            • Fms!-lst
            • Delete-file$
            • *standard-ci*
            • Write-list
            • Trace-co
            • Fmt!
            • Fms
            • Cw!
            • Fmt-to-comment-window!
            • Fms!
            • Eviscerate-hide-terms
            • Fmt1!
            • Fmt-to-comment-window!+
            • Read-file-into-byte-array-stobj
            • Fmt1
            • Fmt-to-comment-window+
            • Cw-print-base-radix!
            • Read-file-into-character-array-stobj
            • Fmx
            • Cw!+
            • Read-objects-from-book
            • Newline
            • Cw+
            • Probe-file
            • Write-objects-to-file!
            • Write-objects-to-file
            • Read-objects-from-file
            • Read-object-from-file
            • Read-file-into-byte-list
            • Set-fmt-soft-right-margin
            • Read-file-into-character-list
            • Io-utilities
          • Defttag
          • Sys-call
          • Save-exec
          • Quicklisp
          • Std/io
          • Oslib
          • Bridge
          • Clex
          • Tshell
          • Unsound-eval
          • Hacker
          • ACL2s-interface
          • Startup-banner
          • Command-line
      • Interfacing-tools
        • Io
          • Fmt
          • Msg
          • Cw
          • Set-evisc-tuple
          • Set-iprint
          • Print-control
          • Read-file-into-string
          • Std/io
          • Msgp
            • Printing-to-strings
            • Evisc-tuple
            • Output-controls
            • Observation
            • *standard-co*
            • Ppr-special-syms
            • Standard-oi
            • Standard-co
            • Without-evisc
            • Serialize
            • Output-to-file
            • Fmt-to-comment-window
            • Princ$
            • Character-encoding
            • Open-output-channel!
            • Cw-print-base-radix
            • Set-print-case
            • Set-print-base
            • Print-object$
            • Extend-pathname
            • Print-object$+
            • Fmx-cw
            • Set-print-radix
            • Set-fmt-hard-right-margin
            • File-write-date$
            • Proofs-co
            • Set-print-base-radix
            • Print-base-p
            • *standard-oi*
            • Wof
            • File-length$
            • Fms!-lst
            • Delete-file$
            • *standard-ci*
            • Write-list
            • Trace-co
            • Fmt!
            • Fms
            • Cw!
            • Fmt-to-comment-window!
            • Fms!
            • Eviscerate-hide-terms
            • Fmt1!
            • Fmt-to-comment-window!+
            • Read-file-into-byte-array-stobj
            • Fmt1
            • Fmt-to-comment-window+
            • Cw-print-base-radix!
            • Read-file-into-character-array-stobj
            • Fmx
            • Cw!+
            • Read-objects-from-book
            • Newline
            • Cw+
            • Probe-file
            • Write-objects-to-file!
            • Write-objects-to-file
            • Read-objects-from-file
            • Read-object-from-file
            • Read-file-into-byte-list
            • Set-fmt-soft-right-margin
            • Read-file-into-character-list
            • Io-utilities
          • Defttag
          • Sys-call
          • Save-exec
          • Quicklisp
          • Std/io
          • Oslib
          • Bridge
          • Clex
          • Tshell
          • Unsound-eval
          • Hacker
          • ACL2s-interface
          • Startup-banner
          • Command-line
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • Io
      • ACL2-built-ins

      Msgp

      Recognizer for a ``message''

      The form (msgp x) evaluates to true when x evaluates either to a string or to a cons whose car is a string and whose cdr satisfies character-alistp. Note that msgp will always hold for the output of the macro msg.

      Function: msgp

      (defun msgp (x)
        (declare (xargs :guard t))
        (or (stringp x)
            (and (consp x)
                 (stringp (car x))
                 (character-alistp (cdr x)))))