Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
ACL2
Theories
Rule-classes
Proof-builder
Recursion-and-induction
Hons-and-memoization
Events
Parallelism
History
Programming
Defun
Declare
System-utilities
Stobj
State
Mutual-recursion
Memoize
Mbe
Io
Defpkg
Apply$
Loop$
Programming-with-state
Arrays
Characters
Time$
Loop$-primer
Fast-alists
Defconst
Defmacro
Evaluation
Guard
Equality-variants
Compilation
Hons
ACL2-built-ins
Let
Declare
Mbe
Apply$
Fmt
Loop$
Return-last
Mv-let
Df
Pseudo-termp
Defwarrant
Time$
Mbt
Ec-call
Mv-nth
Sys-call
Msg
Er
Value-triple
Comp
O-p
Member
O<
Cw
Flet
Cbd
Or
Hons
Mv
Defbadge
Append
*ACL2-exports*
Eql
Comment
Unsigned-byte-p
Posp
Natp
The
Nth
And
Len
List
Time-tracker
Term-order
True-listp
Msgp
Booleanp
<
If
Pseudo-term-listp
+
Not
With-global-stobj
Bitp
Equal
Cdr
Car
String-listp
Nat-listp
Implies
Iff
Character-listp
Alistp
Cons
Symbol-listp
Quote
Create-inst-doc
Opcode
Opcode-fix
Make-opcode
Opcode-p
Opcode-equiv
Change-opcode
Opcode->superscripts
Opcode->group
Opcode->vex
Opcode->r/m
Opcode->reg
Opcode->pfx
Opcode->mode
Opcode->feat
Opcode->evex
Opcode->rex
Opcode->op
Opcode->mod
Select-insts
Inst
Op/en-p
Operands
Operand-type-p
Strict-opcode-p
Opcode-extension-group-p
Create-insts-doc
Create-insts-doc-aux
Superscripts-p
Maybe-operands-p
Inst-list-p
Exception-desc-p
Count-avx-pfx-cases
Mnemonic-p
Maybe-3bits-p
Op-pfx-p
Maybe-vex-p
Maybe-evex-p
Fn-desc-p
Chk-exc-fn
Remove-insts-with-feat
Op-mode-p
Keep-insts-with-feat
Rex-p
Mod-p
Gen-operand-type-code-doc
Gen-addressing-method-code-doc
Create-arg-doc
Create-extra-info-doc
Avx-pfx-well-formed-p
Create-extra-info-doc-string
Create-args-doc
Symbol-list-to-string
Get-operand-type-code-doc
Get-addressing-method-doc
Unquote
Any-present-in
Eval-pre-map
Superscripts-fix
Strict-opcode-fix
Operand-type-fix
Opcode-extension-group-fix
Maybe-operands-fix
Maybe-evex-fix
Maybe-3bits-fix
Keyword-list-fix
Exception-desc-fix
Rex-fix
Op-pfx-fix
Op-mode-fix
Mod-fix
Mnemonic-fix
Maybe-vex-fix
Fn-desc-fix
Vex-p
Evex-p
Integerp
Consp
True-list-listp
State-global-let*
Compress1
Symbolp
Stringp
Macrolet
*common-lisp-symbols-from-main-lisp-package*
Characterp
Prog2$
*
Last-prover-steps
Hons-acons
Eq
Let*
@
With-guard-checking
With-local-stobj
Length
Hard-error
-
Zp
Search
Intersection$
Assign
Aset1
Symbol-name
Union$
Set-gc-strategy
In-tau-intervalp
Break-on-error
Pand
Cons-with-hint
Case-match
Fast-alist-fork
Sys-call+
ACL2-count
Remove-duplicates
Signed-byte-p
With-serialize-character
Observation
Hons-resize
Make-tau-interval
Logbitp
Termp
Position
Assoc
*standard-co*
Hons-acons!
Aref1
Read-run-time
Update-nth
Take
Hons-wash
Symbol-package-name
Expt
Coerce
Keywordp
Intern
Non-exec
Case
Standard-oi
Standard-co
Get-internal-time
Formula
Atom
Without-evisc
Good-bye
With-local-state
Spec-mv-let
Intern-in-package-of-symbol
Hons-clear
Binary-+
Ash
With-fast-alist
Symbol-alistp
Set-difference$
Flush-compress
Rationalp
Por
<=
Rassoc
Remove-assoc
=
Nthcdr
Pargs
Nfix
Hons-copy
Alphorder
Subsetp
Logand
Remove1-assoc
No-duplicatesp
Mv-list
Canonical-pathname
Aset2
Floor
Serialize-read
Random$
Fmt-to-comment-window
F-put-global
Compress2
Concatenate
Fast-alist-clean
Assert$
Remove
Remove1
Intersectp
Endp
Put-assoc
Princ$
Primitive
Keyword-value-listp
True-list-fix
Swap-stobjs
Illegal
Hons-get
With-output-lock
Setenv$
Open-output-channel!
Fast-alist-free
Er-progn
Cw-print-base-radix
Reverse
Cond
Complex
Add-to-set
Truncate
Digit-char-p
Code-char
Set-print-case
Set-print-base
Read-ACL2-oracle
Error1
Print-object$
Plet
Fmx-cw
Integer-length
Zip
With-live-state
Hons-assoc-equal
Extend-pathname
Logior
Char-code
With-guard-checking-event
Term-listp
Print-object$+
String
Mod
In-package
Unary--
Set-print-radix
Resize-list
Pkg-witness
Integer-listp
Revappend
Null
Term-list-listp
Make-fast-alist
Header
Boole$
Subseq
With-guard-checking-error-triple
/
Make-list
Logxor
Char-upcase
Char-downcase
Strip-cars
Set-fmt-hard-right-margin
Make-ord
Ifix
Fast-alist-free-on-exit
F-get-global
Aref2
Standard-char-p
Lognot
Must-be-equal
Integer-range-p
Getenv$
Binary-append
Er-hard
Eqlablep
Cpu-core-count
ACL2-numberp
Butlast
Pairlis$
Mod-expt
Hons-equal
Gc$
Boolean-listp
Substitute
Ceiling
With-stolen-alist
Mv?-let
String-upcase
String-downcase
Round
Count
Char
Sys-call-status
Progn$
Pprogn
Lexorder
Hons-summary
Break$
Assert*
Alpha-char-p
Strip-cdrs
Serialize-write
Keyword-listp
Logeqv
List*
Proofs-co
Maximum-length
Fix
Explode-nonnegative-integer
Eqlable-listp
Dimensions
Default
Arity
Upper-case-p
Sublis
Max
Lower-case-p
Evenp
Explode-atom
Change
Zerop
String<
String-equal
Last
Abs
Set-print-base-radix
Print-base-p
Nonnegative-integer-quotient
Intern$
Getprop
Binary-*
Aset1-trusted
Symbol<
String-append
Rfix
Mv?
Logic-fns-list-listp
Fast-alist-fork!
Er-hard?
Allocate-fixnum-range
Char-equal
1+
*standard-oi*
Sys-call*
Pos-listp
Mbt*
Hons-wash!
Hons-clear!
Signum
Rem
Real/rationalp
Rational-listp
O-first-coeff
Logic-fnsp
Logic-fns-listp
Hons-copy-persistent
Gc-strategy
Fast-alist-summary
String>=
String<=
Acons
O-first-expt
Fast-alist-clean!
>=
>
Subst
Logcount
Getpropc
Evens
Er-soft
Digit-to-char
Comp-gcl
Atom-listp
Arities-okp
ACL2-number-listp
/=
Cadr
*standard-ci*
Unary-/
The-true-list
Realfix
O-rst
Fast-alist-len
Complex/complex-rationalp
Array2p
Array1p
Logtest
Logandc1
Char<
Trace-co
Putprop
Get-real-time
Eqlable-alistp
Count-keys
Assoc-string-equal
Logorc1
Logandc2
1-
Packn
Logic-termp
Logic-term-list-listp
Fmt!
Fms
Cw!
Assoc-keyword
String>
Numerator
Logorc2
Denominator
Char>=
The-number
Odds
Makunbound-global
Make-character-list
Make
Get-cpu-time
Fmt-to-comment-window!
Fms!
F-boundp-global
Complex-rationalp
Alist-to-doublets
Access
Min
Lognor
Listp
Identity
Char>
Char<=
Zpf
Update-nth-array
Standard-char-listp
O-finp
Number-subtrees
Logic-term-listp
Last-cdr
Fmt1!
Fmt-to-comment-window!+
Character-alistp
Oddp
Minusp
Lognand
Imagpart
Conjugate
Xor
Unquote
String-alistp
Packn-pos
Maybe-flush-and-compress1
Kwote
Int=
Fmt1
Fmt-to-comment-window+
Cw-print-base-radix!
Alist-keys-subsetp
Realpart
Plusp
First
Symbol-name-lst
R-symbol-alistp
R-eqlable-alistp
Fmx
Cw!+
Cons-subtrees
Cons-count-bounded
Cddr
Caar
Proper-consp
Kwote-lst
Improper-consp
Cw+
Rest
Standard-char-p+
Mbe1
Caddr
Pairlis-x2
Pairlis-x1
O>=
O<=
O-infp
Merge-sort-lexorder
Fix-true-list
Cdddr
Set-fmt-soft-right-margin
Real-listp
O>
Cddar
Cdar
Cdadr
Cdaar
Cadar
Caadr
Caaar
Cadddr
Caddar
Third
Tenth
Sixth
Seventh
Second
Ninth
Fourth
Fifth
Eighth
Cddddr
Cdddar
Cddadr
Cddaar
Cdaddr
Cdadar
Cdaadr
Cdaaar
Cadadr
Cadaar
Caaddr
Caadar
Caaadr
Caaaar
Hons-shrink-alist!
Hons-shrink-alist
Flush-hons-get-hash-table-link
Delete-assoc
Developers-guide
System-attachments
Advanced-features
Set-check-invariant-risk
Numbers
Irrelevant-formals
Efficiency
Introduction-to-programming-in-ACL2-for-those-who-know-lisp
Redefining-programs
Lists
Invariant-risk
Errors
Defabbrev
Conses
Alists
Set-register-invariant-risk
Strings
Program-wrapper
Get-internal-time
Basics
Packages
Oracle-eval
Defmacro-untouchable
Primitive
<<
Revert-world
Set-duplicate-keys-action
Unmemoize
Symbols
Def-list-constructor
Easy-simplify-term
Defiteration
Fake-oracle-eval
Defopen
Sleep
Operational-semantics
Real
Start-here
Debugging
Miscellaneous
Output-controls
Macros
Interfacing-tools
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Quote
Opcode-maps-structures
Opcode
This is a product type introduced by
defprod
.
Fields
op —
24bits
Includes escape bytes of two- and three-byte opcodes as well
mode —
op-mode
reg —
maybe-3bits
ModR/M.reg descriptor
mod —
mod
ModR/M.mod descriptor
r/m —
maybe-3bits
ModR/M.r/m descriptor
pfx —
op-pfx
rex —
rex
REX descriptor
vex —
maybe-vex
evex —
maybe-evex
feat —
ACL2::symbol-list
superscripts —
superscripts
group —
opcode-extension-group
Subtopics
Opcode-fix
Fixing function for
opcode
structures.
Make-opcode
Basic constructor macro for
opcode
structures.
Opcode-p
Recognizer for
opcode
structures.
Opcode-equiv
Basic equivalence relation for
opcode
structures.
Change-opcode
Modifying constructor for
opcode
structures.
Opcode->superscripts
Get the
superscripts
field from a
opcode
.
Opcode->group
Get the
group
field from a
opcode
.
Opcode->vex
Get the
vex
field from a
opcode
.
Opcode->r/m
Get the
r/m
field from a
opcode
.
Opcode->reg
Get the
reg
field from a
opcode
.
Opcode->pfx
Get the
pfx
field from a
opcode
.
Opcode->mode
Get the
mode
field from a
opcode
.
Opcode->feat
Get the
feat
field from a
opcode
.
Opcode->evex
Get the
evex
field from a
opcode
.
Opcode->rex
Get the
rex
field from a
opcode
.
Opcode->op
Get the
op
field from a
opcode
.
Opcode->mod
Get the
mod
field from a
opcode
.