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
Check-mv-let-call
Term-possible-numbers-of-results
Check-user-term
Check-nary-lambda-call
Check-lambda-call
All-vars-open
Dumb-occur-var-open
Check-user-lambda
Check-if-call
One-way-unify$
Check-unary-lambda-call
Guard-verified-fnsp
All-non-gv-ffn-symbs
All-non-gv-ffn-symbs-lst
All-non-gv-exec-ffn-symbs
Check-fn-call
Guard-verified-exec-fnsp
Check-list-call
Check-or-call
Check-and-call
All-program-ffn-symbs
Lambda-guard-verified-fnsp
All-free/bound-vars
Check-mbt$-call
If-tree-leaf-terms
Check-not-call
Check-mbt-call
Term-guard-obligation
All-pkg-names
All-vars-in-untranslated-term
Std/system/all-fnnames
Lambda-logic-fnsp
Lambda-guard-verified-exec-fnsp
All-lambdas
Lambda-closedp
Std/system/all-vars
Std/system/term-transformations
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
All-non-gv-ffn-symbs
All-non-gv-ffn-symbs-lst
Signature
(all-non-gv-ffn-symbs-lst terms ans wrld) → final-ans
Arguments
terms
—
Guard
(
pseudo-term-listp
terms)
.
ans
—
Guard
(
symbol-listp
ans)
.
wrld
—
Guard
(
plist-worldp
wrld)
.
Returns
final-ans
—
Type
(
symbol-listp
final-ans)
, given the
guard
.