Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Kestrel-books
Crypto-hdwallet
Apt
Error-checking
Abnf
Fty-extensions
Isar
Kestrel-utilities
Soft
Bv
Imp-language
Event-macros
C
Atc
Syntax-for-tools
Disambiguator
Abstract-syntax
Parser
Parse-exprs/decls
Parstate
Parse-stmts/blocks
Check-full-ppnumber
Read-char
Lex-oct-iconst-/-dec-fconst
Lex-lexeme
Parse-external-declaration
Parse-cast-expression
Lex-isuffix-if-present
Lex-identifier/keyword
Parse-postfix-expression
Lex-hex-iconst/fconst
Lex-dec-iconst/fconst
Lex-block-comment
Lex-escape-sequence
Parse-declaration-or-statement
Token
Read-token
Parse-declaration
Lex-*-hexadecimal-digit
Lex-*-c-char
Lex-*-s-char
Parse-specifier/qualifier
Lex-*-digit
Lex-line-comment
Char-to-msg
Parstate$
Parse-pointer
Parse-declaration-specifier
Lex-iconst/fconst
Parse-expression-or-type-name
Parse-external-declaration-list
Parse-declaration-specifiers
Lex-dec-expo-if-present
Parse-asm-name-specifier
Lex-character-constant
Parse-expression-rest
Lex-dec-fconst
Token-unary-expression-start-p
Parse-declarator-or-abstract-declarator
Lex-stringlit
Lex-non-octal-digit
Position
Lexeme
Lexeme-case
Lexeme-fix
Lexeme-equiv
Lexemep
Lexeme-token
Lexeme-token->unwrap
Make-lexeme-token
Change-lexeme-token
Lexeme-whitespace
Lexeme-comment
Lexeme-kind
Lex-fsuffix-if-present
Init-parstate
Parse-type-qualifier-list
Lex-hexadecimal-digit
Parse-translation-unit
Token-postfix-expression-rest-start-p
Parse-?-asm-name-specifier
Parse-postfix-expression-rest
Parse-expression
Lex-sign-if-present
Lex-dec-expo
Lex-bin-expo
Parse-*-stringlit
Parse-statement
Parse-fileset
Parse-declaration-list
Make-expr-unary-with-preinc/predec-ops
Parse-init-declarator-list
Token-type-specifier-keyword-p
Token-option
Lexeme-option
Parse-*-attribute-specifier
Parse-initializer-list
Parse-init-declarator
Parse-file
Unread-token
Parse-array/function-declarator
Span
Read-stringlit
Lex-hex-quad
Unread-char
Read-identifier
Parse-argument-expressions
Make-expr-cast/add-or-cast/sub-ambig
Read-punctuator
Parse-assignment-expression
Token-type-qualifier-p
Token-struct-declaration-start-p
Token-specifier/qualifier-start-p
Token-function-specifier-p
Reterr-msg
Read-keyword
Parse-*-increment/decrement
Parse-direct-abstract-declarator
Char+position
Update-parstate->tokens-unread
Update-parstate->tokens-read-len
Update-parstate->chars-unread
Token+span
Token-expression-start-p
Parse-primary-expression
Backtrack-checkpoint
Update-parstate->tokens-read
Update-parstate->checkpoints
Update-parstate->chars-read
Token-to-msg
Update-parstate->position
Parse-parameter-declaration
Parse-argument-expressions-rest
Token-primary-expression-start-p
Clear-checkpoint
Update-parstate->bytes
Parse-unary-expression
Parse-generic-associations-rest
Update-parstate->size
Update-parstate->gcc
Token-to-type-specifier-keyword
Token-declaration-specifier-start-p
Parsize
Parse-direct-abstract-declarator-rest
Parse-designator-list
Unread-tokens
Unread-chars
Token-designation?-initializer-start-p
Token-abstract-declarator-start-p
Record-checkpoint
Parse-struct-declaration
Parse-specifier-qualifier-list
Parse-parameter-declaration-list
Parse-constant-expression
Parse-conditional-expression
Token-type-specifier-start-p
Parse-static-assert-declaration
Parse-fileset-loop
Parse-direct-declarator
Parse-attribute-parameters
Token-unary-operator-p
Token-to-unary-operator
Token-storage-class-specifier-p
Token-punctuatorp
Token-direct-abstract-declarator-start-p
Token-declarator-start-p
Parse-direct-declarator-rest
Token-to-storage-class-specifier
Token-to-assignment-operator
Token-struct-declarator-start-p
Token-keywordp
Token-initializer-start-p
Token-direct-declarator-start-p
Token-assignment-operator-p
Parstate->tokens-unread
Parse-struct-or-union-specifier
Parse-enumerator-list
Parse-designation?-initializer
Parse-block-item
Token-type-name-start-p
Token-to-type-qualifier
Token-to-function-specifier
Token-preinc/predec-operator-p
Token-multiplicative-operator-p
Token-designator-start-p
Token-designation-start-p
Parstate->tokens-read-len
Parstate->tokens-read
Parstate->checkpoints
Parstate->chars-unread
Parstate->chars-read
Parstate->bytes
Parse-initializer
Parse-generic-association
Parse-attribute-specifier
Token-to-relational-operator
Token-to-preinc/predec-operator
Token-to-multiplicative-operator
Token-relational-operator-p
Token-equality-operator-p
Token-additive-operator-p
Span-join
Parstate->size
Parstate->position
Parse-compound-literal
Token-to-equality-operator
Token-to-additive-operator
Token-shift-operator-p
Position-inc-line
Position-inc-column
Parstate->gcc
Parse-type-name
Parse-struct-declarator-list
Parse-struct-declaration-list
Parse-relational-expression-rest
Parse-multiplicative-expression-rest
Parse-logical-or-expression-rest
Parse-logical-and-expression-rest
Parse-inclusive-or-expression-rest
Parse-exclusive-or-expression-rest
Parse-equality-expression-rest
Parse-array/function-abstract-declarator
Parse-additive-expression-rest
Token-to-shift-operator
Parse-struct-declarator
Parse-shift-expression-rest
Parse-and-expression-rest
Parse-alignment-specifier
Position-to-msg
Parse-shift-expression
Parse-relational-expression
Parse-multiplicative-expression
Parse-logical-or-expression
Parse-logical-and-expression
Parse-inclusive-or-expression
Parse-exclusive-or-expression
Parse-equality-expression
Parse-enum-specifier
Parse-block-item-list
Parse-attribute-list
Parse-and-expression
Parse-additive-expression
Parse-abstract-declarator
Char+position-list
Token+span-list
Span-to-msg
Position-init
Parstate-fix
Parse-designator
Parse-declarator
Parse-attribute
Irr-token
Irr-span
Irr-position
Irr-lexeme
Token-list
To-parstate$
Parse-enumerator
Printer
Formalized-subset
Mapping-to-language-definition
Output-files
Input-files
Validator
Implementation-environments
Concrete-syntax
Preprocessing
Language
Representation
Transformation-tools
Pack
Java
Bitcoin
Ethereum
Yul
Zcash
ACL2-programming-language
Prime-fields
Json
Syntheto
File-io-light
Number-theory
Cryptography
Lists-light
Builtins
Axe
Solidity
Helpers
Std-extensions
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Lexeme
Lexeme-token
This is a product type, introduced by
fty::deftagsum
in support of
lexeme
.
Fields
unwrap —
token
Subtopics
Lexeme-token->unwrap
Get the
unwrap
field from a
lexeme-token
.
Make-lexeme-token
Basic constructor macro for
lexeme-token
structures.
Change-lexeme-token
Modifying constructor for
lexeme-token
structures.