Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Recursion-and-induction
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
B*
Defunc
Fty
Deftagsum
Defprod
Defflexsum
Defbitstruct
Deflist
Defalist
Defbyte
Defresult
Deffixtype
Deffixequiv
Fty-discipline
Defoption
Fty-extensions
Defsubtype
Deftypes
Defflatsum
Deflist-of-len
Defbytelist
Defset
Fty::basetypes
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
Nat-set
Bit-list
Defvisitors
Deffixtype-alias
Defomap
Deffixequiv-sk
Defunit
Deffixequiv-mutual
Fty::baselists
Defmap
Std/util
Apt
Defdata
Defrstobj
Seq
Match-tree
Defrstobj
With-supporters
Def-partial-measure
Template-subst
Soft
Defthm-domain
Event-macros
Def-universal-equiv
Def-saved-obligs
With-supporters-after
Definec
Sig
Outer-local
Data-structures
ACL2
Interfacing-tools
Hardware-verification
Software-verification
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.
Nat-set
Fixtype of finite sets of natural numbers.
Bit-list
A
fixtype
of true lists of
bits
.
