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
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
Type-definition-list-fix
Type-definition-list-equiv
Type-definition-listp
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
Helpers
Std-extensions
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Abstract-syntax
Type-definition-list
Fixtype of lists of Syntheto type definitions.
This is an ordinary
fty::deflist
.
Subtopics
Type-definition-list-fix
(type-definition-list-fix x)
is a usual
ACL2::fty
list fixing function.
Type-definition-list-equiv
Basic equivalence relation for
type-definition-list
structures.
Type-definition-listp
(type-definition-listp x)
recognizes lists where every element satisfies
type-definitionp
.