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