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
Java
Bitcoin
Ethereum
Yul
Zcash
ACL2-programming-language
Prime-fields
Json
Syntheto
Process-syntheto-toplevel-fn
Translation
Language
Static-semantics
Abstract-syntax
Expression
Expression-sum-field-list
Type
Typep
Type-case
Type-fix
Type-count
Type-equiv
Type-map
Type-set
Type-sequence
Type-sequence->element
Make-type-sequence
Change-type-sequence
Type-defined
Type-option
Type-kind
Type-string
Type-integer
Type-character
Type-boolean
Binary-op
Expression-product-field-list
Abstract-syntax-operations
Function-definition-list->header-list
Type-definition-list->name-list
Initializer-list->value-list
Function-header-list->name-list
Typed-variable-list->type-list
Typed-variable-list->name-list
Branch-list->condition-list
Alternative-list->name-list
Function-specifier
Expression-variable-list
Type-subset
Field-list->type-list
Field-list->name-list
Function-specification
Identifier
Toplevel
Function-definer
Function-header
Type-definer
Literal
Type-product
Function-definition
Type-sum
Maybe-expression
Transform-argument-value
Transform
Theorem
Quantifier
Maybe-function-specification
Maybe-typed-variable
Maybe-type-definition
Maybe-function-header
Maybe-function-definition
Maybe-type-sum
Maybe-type-subset
Maybe-type-product
Maybe-type-definer
Maybe-theorem
Maybe-type
Initializer
Type-definition
Alternative
Unary-op
Typed-variable
Branch
Field
Transform-argument
Type-recursion
Program
Function-recursion
Typed-variable-list
Toplevel-name
Toplevel-list
Initializer-list
Expression-fixtypes
Toplevel-fn-names
Lookup-transform-argument
Function-definition-names
Type-definition-list
Transform-argument-list
Function-header-list
Function-definition-list
Alternative-list
Type-list
Identifier-set
Identifier-list
Field-list
Expression-list
Branch-list
Extract-default-param-alist
Create-arg-defaults-table
Outcome
Abstract-syntax-operations
Outcome-list
Outcomes
Process-syntheto-toplevel
Shallow-embedding
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
Type
Type-sequence
This is a product type, introduced by
fty::deftagsum
in support of
type
.
Fields
element —
type
Subtopics
Type-sequence->element
Get the
element
field from a
type-sequence
.
Make-type-sequence
Basic constructor macro for
type-sequence
structures.
Change-type-sequence
Modifying constructor for
type-sequence
structures.