Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Std/lists
Std/alists
Obags
Std/util
Std/strings
Std/io
Std/osets
Std/basic
Std/system
Fresh-logical-name-with-$s-suffix
Irrelevant-formals-info
Std/system/function-queries
Std/system/term-queries
Std/system/term-transformations
Make-mv-let-call
Mvify
Remove-trivial-vars
Remove-unused-vars
Remove-unused-vars-aux
Remove-unused-vars-lst
Fsublis-fn-rec
Close-lambdas
Fsublis-var
Remove-mbe-logic/exec
Untranslate$
Remove-dead-if-branches
Remove-progn
Make-mv-nth-calls
Apply-fn-into-ifs
Conjoin-equalities
Fapply-unary-to-terms
Apply-unary-to-terms
Apply-terms-same-args
Apply-term
Fsublis-fn-lst-simple
Fsublis-fn
Fapply-terms-same-args
Fsublis-fn-simple
Fapply-term
Remove-mbe-logic
Remove-mbe-exec
Quote-term
Quote-term-list
Apply-term*
Std/system/fsubcor-var
Std/system/conjoin
Std/system/flatten-ands-in-lit
Fapply-term*
Std/system/dumb-negate-lit
Std/system/enhanced-utilities
Install-not-normalized-event
Install-not-normalized-event-lst
Std/system/term-function-recognizers
Genvar$
Std/system/event-name-queries
Pseudo-tests-and-call-listp
Maybe-pseudo-event-formp
Add-suffix-to-fn-or-const
Chk-irrelevant-formals-ok
Table-alist+
Pseudo-tests-and-callp
Add-suffix-to-fn-or-const-lst
Known-packages+
Add-suffix-to-fn-lst
Unquote-term
Event-landmark-names
Add-suffix-lst
Std/system/theorem-queries
Unquote-term-list
Std/system/macro-queries
Pseudo-command-landmark-listp
Install-not-normalized$
Pseudo-event-landmark-listp
Known-packages
Std/system/partition-rest-and-keyword-args
Rune-enabledp
Rune-disabledp
Included-books
Std/system/pseudo-event-formp
Std/system/plist-worldp-with-formals
Std/system/w
Std/system/geprops
Std/system/arglistp
Std/system/constant-queries
Std/typed-lists
Std/bitsets
Std/testing
Std/typed-alists
Std/stobjs
Std-extensions
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Remove-unused-vars
Remove-unused-vars-lst
Signature
(remove-unused-vars-lst terms) → new-terms
Arguments
terms
—
Guard
(
pseudo-term-listp
terms)
.
Returns
new-terms
—
Type
(
and
(
pseudo-term-listp
new-terms) (
equal
(
len
new-terms) (
len
terms)))
, given the
guard
.