Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Recursion-and-induction
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Kestrel-books
Crypto-hdwallet
Error-checking
Apt
Abnf
Fty-extensions
Defbyte
Defresult
Defsubtype
Pos-list
Defflatsum
Deflist-of-len
Defbytelist
Specific-types
Pos-list
Defbyte-standard-instances
Defbytelist-standard-instances
Byte-list
Byte
Nibble
Pos-option
Nat-option
Byte-list20
String-option
Byte-list32
Byte-list64
Pseudo-event-form
Character-list
Natoption/natoptionlist
Nati
Maybe-string
Nat/natlist
Nibble-list
Natoption/natoptionlist-result
Set
Nat/natlist-result
Nat-option-list-result
String-result
String-list-result
Nat-result
Nat-option-result
Nat-list-result
Maybe-string-result
Integer-result
Character-result
Character-list-result
Boolean-result
Map
Bag
Pseudo-event-form-list
Nat-option-list
Symbol-set
Nat-set
Bit-list
Defset
Defbyte-standard-instances
Deffixtype-alias
Defomap
Defbytelist-standard-instances
Defunit
Byte-list
Byte
Nibble
Pos-option
Nat-option
Byte-list20
String-option
Byte-list32
Byte-list64
Pseudo-event-form
Character-list
Natoption/natoptionlist
Nati
Maybe-string
Nat/natlist
Nibble-list
Natoption/natoptionlist-result
Set
Nat/natlist-result
Nat-option-list-result
String-result
String-list-result
Nat-result
Nat-option-result
Nat-list-result
Maybe-string-result
Integer-result
Character-result
Character-list-result
Boolean-result
Map
Bag
Pseudo-event-form-list
Nat-option-list
Symbol-set
Nat-set
Bit-list
Isar
Kestrel-utilities
Prime-field-constraint-systems
Soft
Bv
Imp-language
Event-macros
Bitcoin
Ethereum
Yul
Zcash
ACL2-programming-language
Prime-fields
Java
C
Syntheto
Number-theory
Cryptography
Lists-light
File-io-light
Json
Built-ins
Solidity
Axe
Std-extensions
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Execloader
Axe
Testing-utilities
Math
Fty-extensions
Fty
Specific-types
Various specific
fixtypes
.
These complement the
base types
and the
base list types
.
Subtopics
Pos-list
Fixtype of lists of positive integers.
Defbyte-standard-instances
Standard fixtypes of unsigned and signed bytes of various sizes, with some accompanying theorems.
Defbytelist-standard-instances
Standard fixtypes of true lists of unsigned and signed bytes of various sizes, with some accompanying theorems.
Byte-list
A
fixtype
of true lists of
(unsigned 8-bit) bytes
.
Byte
A
fixtype
of
(unsigned 8-bit) bytes
.
Nibble
A
fixtype
of
(unsigned 4-bit) nibbles
.
Pos-option
Fixtype of optional positive integer numbers.
Nat-option
Fixtype of optional natural numbers.
Byte-list20
A
fixtype
of true lists of
(unsigned 8-bit) bytes
of length 20.
String-option
Fixtype of optional strings.
Byte-list32
A
fixtype
of true lists of
(unsigned 8-bit) bytes
of length 32.
Byte-list64
A
fixtype
of true lists of
(unsigned 8-bit) bytes
of length 64.
Pseudo-event-form
Fixtype of pseudo event forms.
Character-list
Fixtype of lists of characters.
Natoption/natoptionlist
Fixtype of optional natural numbers and lists of optional natural numbers.
Nati
A
fixtype of natural numbers and infinity.
Maybe-string
Fixtype of optional strings.
Nat/natlist
Fixtype of natural numbers and lists of natural numbers.
Nibble-list
A
fixtype
of true lists of
(unsigned 4-bit) nibbles
.
Natoption/natoptionlist-result
Fixtype of errors and optional natural numbers and lists of optional natural numbers.
Set
A
fixtype
of
osets
.
Nat/natlist-result
Fixtype of errors and natural numbers and lists or natural numbers.
Nat-option-list-result
Fixtype of errors and lists of optional natural numbers.
String-result
Fixtype of errors and strings.
String-list-result
Fixtype of errors and lists of strings.
Nat-result
Fixtype of errors and natural numbers.
Nat-option-result
Fixtype of errors and optional natural numbers.
Nat-list-result
Fixtype of errors and lists of natural numbers.
Maybe-string-result
Fixtype of errors and optional strings.
Integer-result
Fixtype of errors and integers.
Character-result
Fixtype of errors and characters.
Character-list-result
Fixtype of errors and lists of characters.
Boolean-result
Fixtype of errors and booleans.
Map
A
fixtype
of
omaps
.
Bag
A
fixtype
of
obags
.
Pseudo-event-form-list
Fixtype of lists of pseudo event forms.
Nat-option-list
Fixtype of lists of optional natural numbers.
Symbol-set
Fixtype of finite sets of symbols.
Nat-set
Fixtype of finite sets of natural numbers.
Bit-list
A
fixtype
of true lists of
bits
.
