• 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
        • 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
    • 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
  • Example-lexer

Token-p

Representation of a single token.

(token-p x) is a defaggregate of the following fields.

  • type — Invariant (tokentype-p type).
  • text — Invariant (stringp text).

Source link: token-p

I make these tagless and illegible so that they're more compact, which is useful when running the examples.

Subtopics

Token
Raw constructor for token-p structures.
Make-token
Constructor macro for token-p structures.
Change-token
A copying macro that lets you create new token-p structures, based on existing structures.
Make-honsed-token
Constructor macro for honsed token-p structures.
Honsed-token
Raw constructor for honsed token-p structures.
Token->type
Access the type field of a token-p structure.
Token->text
Access the text field of a token-p structure.