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
Atj
Atj-implementation
Atj-types
Atj-type-<=
Atj-function-type
Atj-type-to-jitype
Atj-type
Atj-function-type-of-min-input-types
Atj-type-top-join
Atj-atype
Atj-type-bottom-meet
Atj-type-bottom-<=
Atj-type-top-<=
Atj-type-top-list-join
Atj-type-bottom-list-<=
Atj-type-top-list-<=
Atj-type-bottom-list-meet
Atj-type-list-<=
Atj-type-to-pred
Atj-maybe-function-type-info
Atj-atype-<=
Atj-maybe-function-type
Atj-maybe-type
Atj-type-to-keyword
Atj-function-type-info
Atj-type-list-join
Atj-type-list-to-type
Atj-type-list-<
Atj-type-list-meet
Atj-type-from-keyword
Atj-function-type-of-min-input-types-aux
Atj-type-<
Atj-type-list-to-type-list-list
Atj-number-of-results
Atj-function-type-info-default
Atj-type-to-pred-gen-mono-thms-2
Atj-get-function-type-info-from-table
Atj-get-function-type-info
Atj-type-to-pred-gen-mono-thms-1
Atj-type-to-pred-gen-mono-thm
Atj-type-meet
Atj-type-to-type-list
Atj-type-list-to-jitype-list
Atj-type-join
Atj-type-of-value
Atj-type-list-to-keyword-list
Atj-type-semilattices
Atj-type-to-pred-gen-mono-thms
Atj-function-type-info->outputs
Atj-function-type-list->outputs
Atj-function-type-list->inputs
Atj-type-list-from-keyword-list
Atj-type-irrelevant
Atj-symbol-type-alist
Atj-type-list
Atj-type-listp
Atj-type-list-fix
Atj-type-list-equiv
Atj-function-type-list
Atj-type-list-list
Atj-maybe-type-list
Atj-function-type-info-table
*atj-function-type-info-table-name*
Atj-java-primitive-array-model
Atj-java-abstract-syntax
Atj-input-processing
Atj-java-pretty-printer
Atj-code-generation
Atj-java-primitives
Atj-java-primitive-arrays
Atj-type-macros
Atj-java-syntax-operations
Atj-fn
Atj-library-extensions
Atj-java-input-types
Atj-test-structures
Aij-notions
Atj-macro-definition
Atj-tutorial
Aij
Language
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
Atj-types
Atj-type-list
Fixtype of lists of ATJ types.
This is an ordinary
fty::deflist
.
Subtopics
Atj-type-listp
(atj-type-listp x)
recognizes lists where every element satisfies
atj-typep
.
Atj-type-list-fix
(atj-type-list-fix x)
is a usual
ACL2::fty
list fixing function.
Atj-type-list-equiv
Basic equivalence relation for
atj-type-list
structures.