Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
B*
B*-binders
ACL2::patbind-ret
ACL2::patbind-stobj-get
Patbind-match
Patbind-when
Patbind-assocs
Patbind-the
Patbind-nths*
Patbind-er
Patbind-nths
Patbind-macro
Patbind-fun
Patbind-faig
Patbind-run-when
Patbind-pattern
Patbind-mv
Patbind-list*
Patbind-list
Patbind-cmp
Patbind-with-stolen
Patbind-with-fast
Patbind-unless-casematch
Patbind-cons
Patbind-access
Patbind-extract-keyword-args
Patbind-run-unless
Patbind-free-on-exit
Patbind-unless
Patbind-local-stobjs
Patbind-if
Patbind-getargs
Patbind-run-if
Patbind-state-global
Patbind-vl-read-zip-header-ret
Patbind-test-glmc-interp-nonhyps-ret
Patbind-test-glmc-interp-hyps-ret
Patbind-glmc-generic-interp-nonhyps-ret
Patbind-glmc-generic-interp-hyps-ret
Def-b*-binder
Defunc
Fty
Apt
Std/util
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
Operational-semantics
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*
B*-binders
ACL2::patbind-ret
ACL2::patbind-stobj-get
Patbind-match
Patbind-when
Patbind-assocs
Patbind-the
Patbind-nths*
Patbind-er
Patbind-nths
Patbind-macro
Patbind-fun
Patbind-faig
Patbind-run-when
Patbind-pattern
Patbind-mv
Patbind-list*
Patbind-list
Patbind-cmp
Patbind-with-stolen
Patbind-with-fast
Patbind-unless-casematch
Patbind-cons
Patbind-access
Patbind-extract-keyword-args
Patbind-run-unless
Patbind-free-on-exit
Patbind-unless
Patbind-local-stobjs
Patbind-if
Patbind-getargs
Patbind-run-if
Patbind-state-global
Patbind-vl-read-zip-header-ret
Patbind-test-glmc-interp-nonhyps-ret
Patbind-test-glmc-interp-hyps-ret
Patbind-glmc-generic-interp-nonhyps-ret
Patbind-glmc-generic-interp-hyps-ret
Def-b*-binder
Defunc
Fty
Apt
Std/util
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
B*
B*-binders
List of the available directives usable in
b*
Subtopics
ACL2::patbind-ret
b*
binder for named return values from functions.
ACL2::patbind-stobj-get
Syntactic sugar for using stobj-let to get some fields from a sub-stobj.
Patbind-match
b*
binder for regular expression matching.
Patbind-when
b*
control flow operator.
Patbind-assocs
b*
binder for extracting particular values from an alist.
Patbind-the
b*
type declaration operator.
Patbind-nths*
b*
binder for list decomposition, using
nth
, with one final
nthcdr
.
Patbind-er
b*
binder for error triples.
Patbind-nths
b*
binder for list decomposition, using
nth
.
Patbind-macro
b*
binder to produce
macrolet
forms.
Patbind-fun
b*
binder to produce
flet
forms.
Patbind-faig
b*
binder that binds two variables to the onset and offset, respectively, of the
faig-fix
of the given expression.
Patbind-run-when
b*
conditional execution operator.
Patbind-pattern
b* binder for JSON pattern matching.
Patbind-mv
b*
binder for multiple values.
Patbind-list*
b*
binder for
list*
decomposition using
car
/
cdr
.
Patbind-list
b*
binder for list decomposition, using
car
/
cdr
.
Patbind-cmp
b*
binder for context-message pairs.
Patbind-with-stolen
b*
binder for invoking
with-stolen-alists
for the remainder of a
b*
form.
Patbind-with-fast
b*
binder to make some alists fast for the remainder of the
b*
form.
Patbind-unless-casematch
b*
binder for using
case-match
against a single pattern.
Patbind-cons
b*
binder for decomposing a
cons
into its
car
and
cdr
.
Patbind-access
b*
binder for accessing record structure fields introduced with ACL2's
defrec
.
Patbind-extract-keyword-args
b*
binder for getargs on a keyword alist.
Patbind-run-unless
b*
conditional execution operator.
Patbind-free-on-exit
b*
binder for freeing fast alists when the
b*
exits.
Patbind-unless
b*
control flow operator.
Patbind-local-stobjs
b*
binder for
with-local-stobj
declarations.
Patbind-if
b*
control flow operator.
Patbind-getargs
b*
binder for getargs on a keyword alist.
Patbind-run-if
b*
conditional execution operator.
Patbind-state-global
b*
binder for accessing state globals.
Patbind-vl-read-zip-header-ret
Patbind-test-glmc-interp-nonhyps-ret
Patbind-test-glmc-interp-hyps-ret
Patbind-glmc-generic-interp-nonhyps-ret
Patbind-glmc-generic-interp-hyps-ret
