|
|
|---|
|
|
|
|---|
An extension of *ACL2-exports* that includes the names of many system-level ACL2 functions.
It is common practice to import all symbols from *ACL2-exports* into one's package; see defpkg. However, those who
write ACL2 system-level programming utilities may prefer to import the symbols
from the list
NOTE To ensure that
(include-book "system/acl2-system-exports" :dir :system)
Here are the symbols added to
(*0* *nil*
*t* *ts-nil* *ts-t* alist-to-doublets
all-calls all-ffn-symbs
all-ffn-symbs-lst arglistp binary-logand
binary-logior binary-logxor body conjoin
cons-count-bounded cons-term cons-term*
defined-constant defun-mode disjoin
disjoin2 dumb-negate-lit enabled-numep
enabled-runep fargn fargs fcons-term
fcons-term* fdefun-mode ffn-symb
ffn-symb-p ffnnamep ffnnamep-lst
find-rules-of-rune flambda-applicationp
flambdap fn-symb formals
fquotep fsubcor-var genvar get-brr-local
get-event get-skipped-proofs-p implicate
lambda-applicationp lambda-body
lambda-formals logicp loop-stopper
make-lambda mbe1 merge-sort-lexorder
merge-sort-term-order
merge-term-order non-linear-arithmetic
normalize nvariablep
pos-listp prettyify-clause programp
proof-builder recursivep rw-cache-state
safe-mode stobjp stobjs-in
stobjs-out subcor-var sublis-var
subst-expr subst-var symbol-class
tag-tree trans-eval translate
translate-cmp translate1 translate1-cmp
translate11 ts= type-alistp
type-set variablep waterfall)