Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
B*
Defunc
Fty
Deftagsum
Defprod
Defflexsum
Defbitstruct
Deflist
Defalist
Defbyte
Deffixequiv
Defresult
Deffixtype
Fty-discipline
Defoption
Fty-extensions
Defbyte
Defresult
Defsubtype
Specific-types
Defset
Defflatsum
Deflist-of-len
Pos-list
Defbytelist
Defbyte-standard-instances
Deffixtype-alias
Defomap
Defbytelist-standard-instances
Defunit
Byte-list
Byte
Pos-option
Nibble
Nat-option
String-option
Byte-list20
Byte-list32
Byte-list64
Pseudo-event-form
Natoption/natoptionlist
Nati
Character-list
Nat/natlist
Maybe-string
Nibble-list
Natoption/natoptionlist-result
Nat/natlist-result
Nat-option-list-result
Set
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
Pos-set
Hex-digit-char-list
Dec-digit-char-list
Nat-option-list
Symbol-set
String-set
Pseudo-event-form-list
Nat-set
Oct-digit-char-list
Bin-digit-char-list
Bit-list
Defsubtype
Specific-types
Deftypes
Defset
Defflatsum
Deflist-of-len
Defbytelist
Fty::basetypes
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
Math
Testing-utilities
Kestrel-books
Fty
Fty-extensions
Extensions of
FTY
in the
Kestrel Books
.
These could be merged with FTY at some point.
Subtopics
Defbyte
Introduce a
fixtype of unsigned or signed bytes of a specified size.
Defresult
Introduce a fixtype for good results and error results.
Defsubtype
Introduce a
fixtype that is a subtype of the given fixtype.
Specific-types
Various specific
fixtypes
.
Defset
Generate a
fixtype of
osets whose elements have a specified fixtype.
Defflatsum
Introduce a fixtype for the flat (i.e. not tagged) sum of disjoint fixtypes.
Deflist-of-len
Introduce a
fixtype of lists of a specified length.
Pos-list
Fixtype of lists of positive integers.
Defbytelist
Introduce a
fixtype of true lists of unsigned or signed bytes of a specified size.
Defbyte-standard-instances
Standard fixtypes of unsigned and signed bytes of various sizes, with some accompanying theorems.
Deffixtype-alias
Introduce an alias of an existing fixtype.
Defomap
Generate a
fixtype of
omaps whose keys and values have specified fixtypes.
Defbytelist-standard-instances
Standard fixtypes of true lists of unsigned and signed bytes of various sizes, with some accompanying theorems.
Defunit
Generate a singleton
fixtype
.
Byte-list
A
fixtype
of true lists of
(unsigned 8-bit) bytes
.
Byte
A
fixtype
of
(unsigned 8-bit) bytes
.
Pos-option
Fixtype of optional positive integer numbers.
Nibble
A
fixtype
of
(unsigned 4-bit) nibbles
.
Nat-option
Fixtype of optional natural numbers.
String-option
Fixtype of optional strings.
Byte-list20
A
fixtype
of true lists of
(unsigned 8-bit) bytes
of length 20.
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.
Natoption/natoptionlist
Fixtype of optional natural numbers and lists of optional natural numbers.
Nati
A
fixtype of natural numbers and infinity.
Character-list
Fixtype of lists of characters.
Nat/natlist
Fixtype of natural numbers and lists of natural numbers.
Maybe-string
Fixtype of optional strings.
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.
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.
Set
A
fixtype
of
osets
.
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
.
Pos-set
Fixtype of finite sets of positive integers.
Hex-digit-char-list
Fixtype of lists of hexadecimal digit characters.
Dec-digit-char-list
Fixtype of lists of decimal digit characters.
Nat-option-list
Fixtype of lists of optional natural numbers.
Symbol-set
Fixtype of finite sets of symbols.
String-set
Fixtype of finite sets of strings.
Pseudo-event-form-list
Fixtype of lists of pseudo event forms.
Nat-set
Fixtype of finite sets of natural numbers.
Oct-digit-char-list
Fixtype of lists of octal digit characters.
Bin-digit-char-list
Fixtype of lists of binary digit characters.
Bit-list
A
fixtype
of true lists of
bits
.