Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
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
Classify-partys/declor/ambig
Lex-dec-iconst/fconst
Lex-block-comment
Lex-escape-sequence
Parse-declaration-or-statement
Token
Lex-*-hexadecimal-digit
Read-token
Parse-declaration
Lex-*-s-char
Lex-*-c-char
Parse-specifier/qualifier
Lex-*-digit
Lex-line-comment
Char-to-msg
Parse-pointer
Parse-expression-or-type-name
Parse-declaration-specifier
Lex-iconst/fconst
Parse-declaration-specifiers
Parse-external-declaration-list
Lex-dec-expo-if-present
Parse-expression-rest
Parse-asm-name-specifier
Token-unary-expression-start-p
Lex-cconst
Partys/declor/ambig
Parse-declarator-or-abstract-declarator
Lex-dec-fconst
Position
Lexeme
Lex-stringlit
Lex-non-octal-digit
Lex-fsuffix-if-present
Token-postfix-expression-rest-start-p
Parse-type-qualifier-list
Parse-translation-unit
Lex-hexadecimal-digit
Parse-statement
Parse-postfix-expression-rest
Parse-fileset
Parse-expression
Make-expr-unary-with-preinc/predec-ops
Parse-declaration-list
Lex-sign-if-present
Lex-dec-expo
Lex-bin-expo
Token-option
Parse-?-asm-name-specifier
Parse-*-stringlit
Parse-init-declarator-list
Lexeme-option
Parse-initializer-list
Parse-*-attribute-specifier
Parse-init-declarator
Span
Parse-array/function-declarator
Parse-file
Read-stringlit
Make-expr-cast/add-or-cast/sub-ambig
Lex-hex-quad
Token-type-qualifier-p
Token-function-specifier-p
Read-identifier
Parse-assignment-expression
Parse-argument-expressions
Unread-token
Token-struct-declaration-start-p
Reterr-msg
Read-punctuator
Char+position
Unread-char
Token+span
Token-expression-start-p
Read-keyword
Parse-*-increment/decrement
Parse-primary-expression
Parse-direct-abstract-declarator
Token-to-msg
Backtrack-checkpoint
Token-specifier/qualifier-start-p
Parse-parameter-declaration
Token-primary-expression-start-p
Parse-argument-expressions-rest
Parse-unary-expression
Parse-generic-associations-rest
Clear-checkpoint
Parsize
Parse-direct-abstract-declarator-rest
Parse-designator-list
Init-parstate
Token-type-specifier-keyword-p
Token-to-type-specifier-keyword
Token-designation?-initializer-start-p
Token-abstract-declarator-start-p
Token-unary-operator-p
Token-type-specifier-start-p
Token-type-name-start-p
Token-to-unary-operator
Token-to-assignment-operator
Record-checkpoint
Parse-struct-declaration
Parse-specifier-qualifier-list
Parse-parameter-declaration-list
Parse-fileset-loop
Parse-constant-expression
Parse-conditional-expression
Unread-tokens
Unread-chars
Token-to-storage-class-specifier
Token-storage-class-specifier-p
Token-direct-abstract-declarator-start-p
Token-declarator-start-p
Token-declaration-specifier-start-p
Parse-static-assert-declaration
Parse-direct-declarator
Parse-attribute-parameters
Token-struct-declarator-start-p
Token-initializer-start-p
Token-direct-declarator-start-p
Token-assignment-operator-p
Parse-direct-declarator-rest
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
Parse-struct-or-union-specifier
Parse-enumerator-list
Parse-designation?-initializer
Parse-block-item
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
Parse-initializer
Parse-generic-association
Token-to-shift-operator
Token-to-equality-operator
Token-to-additive-operator
Token-shift-operator-p
Position-inc-line
Position-inc-column
Parse-compound-literal
Parse-attribute-specifier
Parse-array/function-abstract-declarator
Parse-type-name
Parse-struct-declarator-list
Parse-struct-declaration-list
Parse-shift-expression-rest
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-and-expression-rest
Parse-additive-expression-rest
Irr-partys/declor/ambig
Position-to-msg
Parse-struct-declarator
Parse-logical-or-expression
Parse-logical-and-expression
Parse-inclusive-or-expression
Parse-exclusive-or-expression
Parse-block-item-list
Parse-alignment-specifier
Parse-abstract-declarator
Char+position-list
Token+span-list
Token+span-list-fix
Token+span-list-equiv
Token+span-listp
Span-to-msg
Parse-shift-expression
Parse-relational-expression
Parse-multiplicative-expression
Parse-equality-expression
Parse-enum-specifier
Parse-attribute-list
Parse-and-expression
Parse-additive-expression
Position-init
Irr-token
Irr-span
Irr-position
Irr-parstate
Irr-lexeme
Token-list
Parse-designator
Parse-declarator
Parse-attribute
Parse-enumerator
Printer
Formalized-subset
Mapping-to-language-definition
Output-files
Input-files
Validator
Concrete-syntax
Preprocessing
Implementation-environments
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
Std-extensions
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Parser
Token+span-list
Fixtype of lists of pairs each consisting of a token and a span.
This is an ordinary
fty::deflist
.
Subtopics
Token+span-list-fix
(token+span-list-fix x)
is a usual
ACL2::fty
list fixing function.
Token+span-list-equiv
Basic equivalence relation for
token+span-list
structures.
Token+span-listp
(token+span-listp x)
recognizes lists where every element satisfies
token+span-p
.