Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
B*
Defunc
Fty
Deftagsum
Defprod
Defflexsum
Defbitstruct
Deflist
Defalist
Defbyte
Deffixequiv
Defresult
Deffixtype
Fty-discipline
Defoption
Fty-extensions
Defsubtype
Specific-types
Pos-list
Defbyte-standard-instances
Defbytelist-standard-instances
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
Hex-digit-char-list
Dec-digit-char-list
Pos-set
Nat-option-list
Symbol-set
String-set
Pseudo-event-form-list
Nat-set
Oct-digit-char-list
Bin-digit-char-list
Bit-list
Deftypes
Defflatsum
Defset
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
Theories
Rule-classes
Proof-builder
Recursion-and-induction
Hons-and-memoization
Events
Parallelism
History
Programming
Real
Start-here
Debugging
Miscellaneous
Output-controls
Macros
Make-event
Defmacro
Untranslate-patterns
Tc
Trans*
Macro-aliases-table
Macro-args
Defabbrev
User-defined-functions-table
Trans
Untranslate-for-execution
Add-macro-fn
Check-vars-not-free
Safe-mode
Macro-libraries
B*
Defunc
Fty
Deftagsum
Defprod
Defflexsum
Defbitstruct
Deflist
Defalist
Defbyte
Deffixequiv
Defresult
Deffixtype
Fty-discipline
Defoption
Fty-extensions
Defsubtype
Specific-types
Pos-list
Defbyte-standard-instances
Defbytelist-standard-instances
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
Hex-digit-char-list
Dec-digit-char-list
Pos-set
Nat-option-list
Symbol-set
String-set
Pseudo-event-form-list
Nat-set
Oct-digit-char-list
Bin-digit-char-list
Bit-list
Deftypes
Defflatsum
Defset
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
Trans1
Defmacro-untouchable
Set-duplicate-keys-action
Add-macro-alias
Magic-macroexpand
Defmacroq
Trans!
Remove-macro-fn
Remove-macro-alias
Add-binop
Untrans-table
Trans*-
Remove-binop
Tcp
Tca
Interfacing-tools
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
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
.
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
.
Hex-digit-char-list
Fixtype of lists of hexadecimal digit characters.
Dec-digit-char-list
Fixtype of lists of decimal digit characters.
Pos-set
Fixtype of finite sets of positive integers.
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
.