• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • 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
      • Mailing-lists
      • Interfacing-tools
        • Io
        • Defttag
        • Sys-call
        • Save-exec
        • Quicklisp
        • Std/io
        • Oslib
        • Bridge
        • Clex
          • Example-lexer
            • Token-p
              • Token
                • Make-token
                • Change-token
                • Make-honsed-token
                • Honsed-token
                • Token->type
                • Token->text
              • Lex-punctuation
              • Lex-id/keyword
              • Lex-string
              • Lex-whitespace
              • Lex-comment
              • Lex1
              • Lex-main
              • Lex*
              • Tokenlist-p
              • Letter-char-p
              • Idtail-char-p
              • Whitespace-char-p
              • Number-char-p
              • Tokentype-p
              • Lex*-exec
              • Newline-string
            • Sin
            • Matching-functions
            • Def-sin-progress
          • Tshell
          • Unsound-eval
          • Hacker
          • ACL2s-interface
          • Startup-banner
          • Command-line
      • Macro-libraries
      • Interfacing-tools
        • Io
        • Defttag
        • Sys-call
        • Save-exec
        • Quicklisp
        • Std/io
        • Oslib
        • Bridge
        • Clex
          • Example-lexer
            • Token-p
              • Token
                • Make-token
                • Change-token
                • Make-honsed-token
                • Honsed-token
                • Token->type
                • Token->text
              • Lex-punctuation
              • Lex-id/keyword
              • Lex-string
              • Lex-whitespace
              • Lex-comment
              • Lex1
              • Lex-main
              • Lex*
              • Tokenlist-p
              • Letter-char-p
              • Idtail-char-p
              • Whitespace-char-p
              • Number-char-p
              • Tokentype-p
              • Lex*-exec
              • Newline-string
            • Sin
            • Matching-functions
            • Def-sin-progress
          • Tshell
          • Unsound-eval
          • Hacker
          • ACL2s-interface
          • Startup-banner
          • Command-line
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • Token-p

      Token

      Raw constructor for token-p structures.

      Syntax:

      (token type text)

      This is the lowest-level constructor for token-p structures. It simply conses together a structure with the specified fields.

      Note: It's generally better to use macros like make-token or change-token instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.

      The token-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-token instead.

      Definition

      This is an ordinary constructor function introduced by defaggregate.

      Function: token

      (defun token (type text)
        (declare (xargs :guard (and (tokentype-p type)
                                    (stringp text))))
        (cons type text))