Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Gl
Esim
Vl2014
Sv
Vwsim
Fgl
Fgl-rewrite-rules
Fgl-syntactic-checker-binders
Binder
Fancy-ev
Def-fgl-program
Bind-var
Add-fgl-brewrites
Add-fgl-brewrite
Def-fgl-rewrite
Narrow-equiv
Def-fgl-branch-merge
Add-fgl-rewrites
Fgl-interp-obj
Collect-cmr-rewrites-for-formula-name
Syntax-bind
Fgl-time
Fgl-prog2
Assume
Add-fgl-binder-meta
Add-fgl-primitive
Add-fgl-meta
Add-fgl-branch-merges
Cmr::rewritelist->lhses
Remove-fgl-brewrites
Remove-fgl-branch-merges
Lhses->branch-function-syms
Enable-execution
Abort-rewrite
Syntax-interp
Remove-fgl-rewrites
Lhses->leading-function-syms
Remove-fgl-primitive
Remove-fgl-binder-meta
If!
Disable-execution
Remove-fgl-meta
Fgl-time-fn
Disable-definition
Def-fgl-brewrite
Fgl-function-mode
Fgl-object
Fgl-solving
Fgl-handling-if-then-elses
Fgl-getting-bits-from-objects
Fgl-primitive-and-meta-rules
Fgl-interpreter-overview
Fgl-counterexamples
Fgl-correctness-of-binding-free-variables
Fgl-debugging
Fgl-testbenches
Def-fgl-boolean-constraint
Fgl-stack
Fgl-rewrite-tracing
Def-fgl-param-thm
Def-fgl-thm
Fgl-fast-alist-support
Fgl-array-support
Advanced-equivalence-checking-with-fgl
Fgl-internals
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Add-fgl-brewrites
Add-fgl-brewrite
Alias for
add-fgl-brewrites
that just takes one name.