|
|
|---|
|
|
|
|---|
Symbols that are often imported into new packages to provide easy access to ACL2 functionality.
When you define a new package for your own work with defpkg,
you will usually want to import many symbols from the
The constant
Those who write code using built-in ACL2 functions (see ACL2-built-ins) may wish to import symbols into their package from the large list *ACL2-system-exports*.
(& &allow-other-keys &aux &body &key &optional &rest &whole * *acl2-exports* *common-lisp-specials-and-constants* *common-lisp-symbols-from-main-lisp-package* *main-lisp-package-name* *standard-chars* *standard-ci* *standard-co* *standard-oi* + - / /= 1+ 1- < <-on-others <= = > >= ?-fn @ a! abort! abort-soft abs access accumulated-persistence accumulated-persistence-oops acl2-count acl2-input-channel-package acl2-number-listp acl2-numberp acl2-oracle acl2-output-channel-package acl2-package acl2-unwind-protect acons active-or-non-runep active-runep add-binop add-custom-keyword-hint add-default-hints add-default-hints! add-include-book-dir add-include-book-dir! add-invisible-fns add-ld-keyword-alias add-ld-keyword-alias! add-macro-alias add-macro-fn add-match-free-override add-nth-alias add-override-hints add-override-hints! add-pair add-pair-preserves-all-boundp add-suffix add-suffix-to-fn add-timers add-to-set add-to-set-eq add-to-set-eql add-to-set-equal adjust-ld-history alistp alistp-forward-to-true-listp all-attachments all-boundp all-boundp-preserves-assoc all-vars all-vars1 all-vars1-lst allocate-fixnum-range alpha-char-p alpha-char-p-forward-to-characterp alphorder always$ always$+ and and-macro append append$ append$+ apply$ apply$-guard apply$-lambda apply$-lambda-guard apply$-userfn aref1 aref2 args arities-okp arity array1p array1p-cons array1p-forward array1p-linear array2p array2p-cons array2p-forward array2p-linear aset1 aset1-trusted aset2 ash assert$ assert* assert-event assign assoc assoc-add-pair assoc-eq assoc-eq-equal assoc-eq-equal-alistp assoc-equal assoc-keyword assoc-string-equal assoc2 associativity-of-* associativity-of-+ assume atom atom-listp atom-listp-forward-to-true-listp backchain-limit badge badge-userfn big-clock-entry big-clock-negative-p binary-* binary-+ binary-append bind-free bit bitp boole$ boolean-listp boolean-listp-cons boolean-listp-forward boolean-listp-forward-to-symbol-listp booleanp booleanp-characterp booleanp-compound-recognizer bounded-integer-alistp bounded-integer-alistp-forward-to-eqlable-alistp bounded-integer-alistp2 boundp-global boundp-global1 break$ break-on-error brr brr-evisc-tuple brr@ build-state1 butlast caaaar caaadr caaar caadar caaddr caadr caar cadaar cadadr cadar caddar cadddr caddr cadr canonical-pathname car car-cdr-elim car-cons case case-list case-list-check case-match case-split case-split-limitations case-test cbd cdaaar cdaadr cdaar cdadar cdaddr cdadr cdar cddaar cddadr cddar cdddar cddddr cdddr cddr cdr cdr-cons cdrn ceiling certify-book certify-book! change char char-code char-code-code-char-is-identity char-code-linear char-downcase char-equal char-upcase char< char<= char> char>= character character-alistp character-listp character-listp-append character-listp-coerce character-listp-forward-to-eqlable-listp character-listp-remove-duplicates-eql character-listp-revappend character-listp-string-downcase-1 character-listp-string-upcase1-1 characterp characterp-char-downcase characterp-char-upcase characterp-nth characterp-page characterp-return characterp-rubout characterp-tab check-invariant-risk check-vars-not-free checkpoint-forced-goals checkpoint-summary-limit clause clear-memoize-statistics clear-memoize-table clear-memoize-tables close-input-channel close-output-channel close-trace-file closure code-char code-char-char-code-is-identity code-char-type coerce coerce-inverse-1 coerce-inverse-2 coerce-object-to-state coerce-state-to-object collect$ collect$+ comment community-books commutativity-of-* commutativity-of-+ comp completion-of-* completion-of-+ completion-of-< completion-of-car completion-of-cdr completion-of-char-code completion-of-code-char completion-of-coerce completion-of-complex completion-of-denominator completion-of-imagpart completion-of-intern-in-package-of-symbol completion-of-numerator completion-of-realpart completion-of-symbol-name completion-of-symbol-package-name completion-of-unary-/ completion-of-unary-minus complex complex-0 complex-definition complex-equal complex-implies1 complex-rationalp complex/complex-rationalp compress1 compress11 compress2 compress21 compress211 concatenate cond cond-clausesp cond-macro conjugate cons cons-equal cons-subtrees cons-with-hint consp consp-assoc-equal constraint-info corollary count-keys cpu-core-count ctx ctxp current-package current-theory cw cw! cw!+ cw+ cw-gstack cw-print-base-radix cw-print-base-radix! d< declare decrement-big-clock defabbrev defabsstobj defabsstobj-missing-events defattach defattach-system default default-*-1 default-*-2 default-+-1 default-+-2 default-<-1 default-<-2 default-backchain-limit default-car default-cdr default-char-code default-coerce-1 default-coerce-2 default-coerce-3 default-compile-fns default-complex-1 default-complex-2 default-defun-mode default-defun-mode-from-state default-denominator default-hints default-imagpart default-measure-function default-numerator default-print-prompt default-realpart default-ruler-extenders default-state-vars default-symbol-name default-symbol-package-name default-total-parallelism-work-limit default-unary-/ default-unary-minus default-verify-guards-eagerness default-well-founded-relation defaxiom defbadge defchoose defcong defconst defequiv defevaluator defexec define-pc-atomic-macro define-pc-help define-pc-macro define-pc-meta define-trusted-clause-processor deflabel deflock defmacro defmacro-last defmacro-untouchable defn defnd defpkg defproxy defrec defrefinement defstobj defstub deftheory deftheory-static defthm defthm-std defthmd defthy defttag defun defun$ defun-inline defun-notinline defun-nx defun-sk defun-std defund defund-inline defund-notinline defund-nx defuns defuns-std defwarrant delete-assoc delete-assoc-eq delete-assoc-equal delete-file$ delete-include-book-dir delete-include-book-dir! denominator digit-char-p digit-to-char dimensions disable disable-forcing disable-immediate-force-modep disable-ubt disabledp disassemble$ distributivity dmr-start dmr-stop do$ doc doc! docs doppelganger-apply$-userfn doppelganger-badge-userfn double-rewrite doublet-listp dumb-occur dumb-occur-var duplicates e/d e0-ord-< e0-ordinalp ec-call eighth eliminate-destructors eliminate-irrelevance enable enable-forcing enable-immediate-force-modep encapsulate endp eq eql eqlable-alistp eqlable-alistp-forward-to-alistp eqlable-listp eqlable-listp-forward-to-atom-listp eqlablep eqlablep-recog equal equal-char-code er er-cmp er-hard er-hard? er-let* er-let*-cmp er-progn er-progn-cmp er-progn-fn er-progn-fn@par er-progn@par er-soft er-soft-logic ev$ ev$-list evenp evens event evisc-tuple executable-counterpart-theory exists exit explain-giant-lambda-object explode-atom explode-nonnegative-integer expt expt-type-prescription-non-zero-base extend-pathname extend-pe-table extend-world extra-info f-boundp-global f-get-global f-put-global fast-alist-clean fast-alist-clean! fast-alist-fork fast-alist-fork! fast-alist-free fast-alist-free-on-exit fast-alist-len fast-alist-summary fc-report fertilize fgetprop fifth file-clock file-clock-p file-clock-p-forward-to-integerp file-length$ file-write-date$ finalize-event-user first first-n-ac fix fix-pkg fix-true-list flet floor flush-compress flush-hons-get-hash-table-link fms fms! fms!-to-string fms-to-string fmt fmt! fmt!-to-string fmt-hard-right-margin fmt-soft-right-margin fmt-to-comment-window fmt-to-comment-window! fmt-to-comment-window!+ fmt-to-comment-window+ fmt-to-string fmt1 fmt1! fmt1!-to-string fmt1-to-string fmx fmx!-cw fmx-cw fn-equal fncall-term forall force formula fourth function-symbolp function-theory gag-mode gc$ gc-strategy gc-verbose gcs generalize get-check-invariant-risk get-command-sequence get-cpu-time get-defun-event get-enforce-redundancy get-event-data get-global get-guard-checking get-in-theory-redundant-okp get-output-stream-string$ get-real-time get-register-invariant-risk get-serialize-character get-slow-alist-action get-timer get-wormhole-status getenv$ getprop getprop-default getpropc getprops getprops1 global-table global-table-cars global-table-cars1 global-val good-atom-listp good-bye granularity ground-zero gthm guard guard-obligation guard-theorem hands-off-lambda-objects-theory hard-error has-propsp has-propsp1 header help hide hist hons hons-acons hons-acons! hons-assoc-equal hons-clear hons-clear! hons-copy hons-copy-persistent hons-equal hons-equal-lite hons-get hons-resize hons-resize-fn hons-shrink-alist hons-shrink-alist! hons-summary hons-wash hons-wash! i-am-here i-close i-large i-limited i-small id idates identity if if* iff iff-implies-equal-implies-1 iff-implies-equal-implies-2 iff-implies-equal-not iff-is-an-equivalence ifix ignorable ignore illegal imagpart imagpart-complex immediate-force-modep implies improper-consp in-arithmetic-theory in-package in-tau-intervalp in-theory include-book incompatible incompatible! increment-file-clock increment-timer induct induction-depth-limit initialize-event-user int= integer integer-0 integer-1 integer-abs integer-implies-rational integer-length integer-listp integer-listp-forward-to-rational-listp integer-range-p integer-step integerp intern intern$ intern-in-package-of-symbol intern-in-package-of-symbol-symbol-name intersection$ intersection-eq intersection-equal intersection-theories intersectp intersectp-eq intersectp-equal inverse-of-* inverse-of-+ invisible-fns-table irrelevant keyword-package keyword-value-listp keyword-value-listp-assoc-keyword keyword-value-listp-forward-to-true-listp keywordp keywordp-forward-to-symbolp known-package-alist known-package-alistp known-package-alistp-forward-to-true-list-listp-and-alistp kwote kwote-lst l< lambda lambda$ last last-cdr last-prover-steps ld ld-always-skip-top-level-locals ld-error-action ld-error-triples ld-evisc-tuple ld-history ld-history-entry-error-flg ld-history-entry-input ld-history-entry-stobjs-out ld-history-entry-stobjs-out/value ld-history-entry-user-data ld-history-entry-value ld-keyword-aliases ld-missing-input-ok ld-post-eval-print ld-pre-eval-filter ld-pre-eval-print ld-prompt ld-query-control-alist ld-redefinition-action ld-skip-proofsp ld-user-stobjs-modified-warning ld-verbose legal-case-clausesp len len-update-nth length let let* let-mbe lex-fix lexorder lexp list list* list*-macro list-macro listp local logand logandc1 logandc2 logbitp logcount logeqv logic logic-fns-list-listp logic-fns-listp logic-fnsp logic-term-list-listp logic-term-listp logic-termp logior lognand lognor lognot logorc1 logorc2 logtest logxor loop$ lower-case-p lower-case-p-char-downcase lower-case-p-forward-to-alpha-char-p lowest-terms lp macro-aliases macro-args macrolet magic-ev-fncall main-timer main-timer-type-prescription make make-character-list make-character-list-make-character-list make-event make-fast-alist make-fmt-bindings make-input-channel make-list make-list-ac make-mv-nths make-ord make-output-channel make-summary-data make-tau-interval make-var-lst make-var-lst1 make-wormhole-status makunbound-global max maximum-length may-need-slashes maybe-convert-to-mv maybe-flush-and-compress1 mbe mbt mbt* member member-eq member-equal member-symbol-name memoize memoize-partial memoize-summary memsum meta-extract-contextual-fact meta-extract-formula meta-extract-global-fact meta-extract-global-fact+ meta-extract-rw+-term mfc mfc-ancestors mfc-ap mfc-clause mfc-rdepth mfc-relieve-hyp mfc-rw mfc-rw+ mfc-ts mfc-type-alist mfc-unify-subst mfc-world min minimal-theory minusp mod mod-expt monitor monitor! monitored-runes more more! more-doc msg msgp must-be-equal mutual-recursion mutual-recursion-guardp mv mv-let mv-list mv-nth mv? mv?-let nat-listp natp near-misses needs-slashes never-memoize newline nfix nfix-list nil nil-is-not-circular ninth no-duplicatesp no-duplicatesp-eq no-duplicatesp-equal non-exec nonnegative-integer-quotient nonnegative-product nonzero-imagpart not nqthm-to-acl2 nth nth-0-cons nth-0-read-run-time-type-prescription nth-add1 nth-aliases nth-update-nth nthcdr null number-subtrees numerator o-finp o-first-coeff o-first-expt o-infp o-p o-rst o< o<= o> o>= observation observation-cw oddp odds ok-if oops open-channel-listp open-channel1 open-channel1-forward-to-true-listp-and-consp open-channels-p open-channels-p-forward open-input-channel open-input-channel-any-p open-input-channel-any-p1 open-input-channel-p open-input-channel-p1 open-input-channels open-output-channel open-output-channel! open-output-channel-any-p open-output-channel-any-p1 open-output-channel-p open-output-channel-p1 open-output-channels open-trace-file optimize or or-macro ordered-symbol-alistp ordered-symbol-alistp-add-pair ordered-symbol-alistp-add-pair-forward ordered-symbol-alistp-forward-to-symbol-alistp ordered-symbol-alistp-getprops ordered-symbol-alistp-remove1-assoc-eq otherwise our-digit-char-p override-hints p! pairlis$ pairlis2 pand pargs partial-encapsulate partition-rest-and-keyword-args pbt pc pcb pcb! pcs pe pe! peek-char$ pf pkg-imports pkg-witness pl pl2 plet plist-worldp plist-worldp-forward-to-assoc-eq-equal-alistp plusp pointers pop-timer por position position-ac position-eq position-eq-ac position-equal position-equal-ac positive posp power-eval pprogn pr pr! preprocess prin1$ prin1-with-slashes prin1-with-slashes1 princ$ print-base-p print-cl-cache print-gv print-object$ print-object$+ print-object$-fn print-object$-preserving-case print-rational-as-decimal print-timer profile prog2$ progn progn! progn$ program project-dir-alist proof-tree proofs-co proper-consp props prove pseudo-term-listp pseudo-term-listp-forward-to-true-listp pseudo-termp pso pso! psof psog pspv pstack puff puff* push-timer push-untouchable put-assoc put-assoc-eq put-assoc-eql put-assoc-equal put-global putprop quick-and-dirty-subsumption-replacement-step quit quote quotep quote~ r-eqlable-alistp r-symbol-alistp random$ rassoc rassoc-eq rassoc-equal ratio rational rational-implies1 rational-implies2 rational-listp rational-listp-forward-to-true-listp rationalp rationalp-* rationalp-+ rationalp-expt-type-prescription rationalp-implies-acl2-numberp rationalp-unary-- rationalp-unary-/ read-acl2-oracle read-acl2-oracle-preserves-state-p1 read-byte$ read-char$ read-file-into-string read-file-listp read-file-listp-forward-to-true-list-listp read-file-listp1 read-file-listp1-forward-to-true-listp-and-consp read-files read-files-p read-files-p-forward-to-read-file-listp read-idate read-object read-object-suppress read-object-with-case read-run-time read-run-time-preserves-state-p1 readable-file readable-file-forward-to-true-listp-and-consp readable-files readable-files-listp readable-files-listp-forward-to-true-list-listp-and-alistp readable-files-p readable-files-p-forward-to-readable-files-listp real-listp real/rationalp realfix realpart realpart-complex realpart-imagpart-elim rebuild redef redef! redef+ redef- redo-flat regenerate-tau-database rem remove remove-assoc remove-assoc-eq remove-assoc-equal remove-binop remove-custom-keyword-hint remove-default-hints remove-default-hints! remove-duplicates remove-duplicates-eq remove-duplicates-eql remove-duplicates-equal remove-eq remove-equal remove-guard-holders remove-invisible-fns remove-macro-alias remove-macro-fn remove-nth-alias remove-override-hints remove-override-hints! remove-untouchable remove1 remove1-assoc remove1-assoc-eq remove1-assoc-equal remove1-eq remove1-equal reset-fc-reporting reset-kill-ring reset-ld-specials reset-prehistory reset-print-control resize-list rest restore-memoization-settings retract-world retrieve return-last return-last-table revappend reverse revert-world rewrite-equiv rewrite-lambda-modep rewrite-lambda-objects-theory rewrite-quoted-constant rewrite-stack-limit rfix round rw-cache satisfies save-and-clear-memoization-settings save-exec search second serialize-read serialize-write set-absstobj-debug set-accumulated-persistence set-backchain-limit set-bad-lisp-consp-memoize set-body set-bogus-defun-hints-ok set-bogus-measure-ok set-bogus-mutual-recursion-ok set-brr-evisc-tuple set-case-split-limitations set-cbd set-check-invariant-risk set-checkpoint-summary-limit set-compile-fns set-compiler-enabled set-debugger-enable set-default-backchain-limit set-default-hints set-default-hints! set-deferred-ttag-notes set-difference$ set-difference-eq set-difference-equal set-difference-theories set-duplicate-keys-action set-duplicate-keys-action! set-enforce-redundancy set-equalp-equal set-evisc-tuple set-fast-cert set-fc-criteria set-fc-report-on-the-fly set-fmt-hard-right-margin set-fmt-soft-right-margin set-gag-mode set-gc-strategy set-guard-checking set-guard-msg set-ignore-ok set-in-theory-redundant-okp set-induction-depth-limit set-induction-depth-limit! set-inhibit-er set-inhibit-er! set-inhibit-output-lst set-inhibit-warnings set-inhibit-warnings! set-inhibited-summary-types set-invisible-fns-table set-iprint set-irrelevant-formals-ok set-ld-always-skip-top-level-locals set-ld-error-action set-ld-error-triples set-ld-evisc-tuple set-ld-keyword-aliases set-ld-keyword-aliases! set-ld-missing-input-ok set-ld-post-eval-print set-ld-pre-eval-filter set-ld-pre-eval-print set-ld-prompt set-ld-query-control-alist set-ld-redefinition-action set-ld-skip-proofs set-ld-skip-proofsp set-ld-user-stobjs-modified-warning set-ld-verbose set-let*-abstraction set-let*-abstractionp set-match-free-default set-match-free-error set-measure-function set-non-linear set-non-linearp set-override-hints set-override-hints! set-parallel-execution set-print-base set-print-base-radix set-print-case set-print-circle set-print-clause-ids set-print-escape set-print-gv-defaults set-print-length set-print-level set-print-lines set-print-radix set-print-readably set-print-right-margin set-proofs-co set-prover-step-limit set-raw-mode set-raw-mode-on set-raw-mode-on! set-raw-proof-format set-raw-warning-format set-register-invariant-risk set-rewrite-stack-limit set-ruler-extenders set-rw-cache-state set-rw-cache-state! set-serialize-character set-serialize-character-system set-skip-meta-termp-checks set-skip-meta-termp-checks! set-slow-alist-action set-splitter-output set-standard-co set-standard-oi set-state-ok set-tau-auto-mode set-temp-touchable-fns set-temp-touchable-vars set-timer set-total-parallelism-work-limit set-total-parallelism-work-limit-error set-trace-evisc-tuple set-verify-guards-eagerness set-w set-warnings-as-errors set-waterfall-parallelism set-waterfall-parallelism-hacks-enabled set-waterfall-parallelism-hacks-enabled! set-waterfall-printing set-well-founded-relation set-wormhole-data set-wormhole-entry-code set-write-acl2x setenv$ seventh sgetprop show-accumulated-persistence show-bdd show-bodies show-brr-evisc-tuple show-custom-keyword-hint-expansion show-fc-criteria signed-byte signed-byte-p signum simplify sixth skip-proofs sleep some-slashable spec-mv-let splitter-output stable-under-simplificationp standard-char standard-char-listp standard-char-listp-append standard-char-listp-forward-to-character-listp standard-char-p standard-char-p+ standard-char-p-nth standard-co standard-oi standard-part standard-string-alistp standard-string-alistp-forward-to-alistp standardp start-proof-tree state state-global-let* state-global-let*-cleanup state-global-let*-get-globals state-global-let*-put-globals state-p state-p-implies-and-forward-to-state-p1 state-p1 state-p1-forward state-p1-update-main-timer state-p1-update-nth-2-world step-limit stobj-let stobj-table stop-proof-tree string string-append string-append-lst string-downcase string-downcase1 string-equal string-equal1 string-is-not-circular string-listp string-upcase string-upcase1 string< string<-irreflexive string<-l string<-l-asymmetric string<-l-irreflexive string<-l-transitive string<-l-trichotomy string<= string> string>= stringp stringp-symbol-package-name strip-cars strip-cdrs sublis sublis-fn sublis-fn-lst-simple sublis-fn-simple subseq subseq-list subsequencep subsetp subsetp-eq subsetp-equal subst substitute substitute-ac suitably-tamep-listp sum$ sum$+ summary swap-stobjs symbol symbol-alistp symbol-alistp-forward-to-eqlable-alistp symbol-doublet-listp symbol-equality symbol-listp symbol-listp-forward-to-true-listp symbol-name symbol-name-intern-in-package-of-symbol symbol-name-lst symbol-package-name symbol< symbol<-asymmetric symbol<-irreflexive symbol<-transitive symbol<-trichotomy symbolp symbolp-intern-in-package-of-symbol synp syntactically-clean-lambda-objects-theory syntaxp sys-call sys-call* sys-call+ sys-call-status t table table-alist take tamep tamep-functionp tamep-lambdap tau-data tau-database tau-interval-dom tau-interval-hi tau-interval-hi-rel tau-interval-lo tau-interval-lo-rel tau-intervalp tau-status tau-system tc tca tcp tenth term-list-listp term-listp term-order termination-theorem termp the the-check the-fixnum the-fixnum! the-number the-true-list theory theory-invariant thereis$ thereis$+ third thm time$ time-tracker time-tracker-tau timer-alistp timer-alistp-forward-to-true-list-listp-and-symbol-alistp toggle-inhibit-er toggle-inhibit-er! toggle-inhibit-warning toggle-inhibit-warning! toggle-pc-macro top-level trace! trace$ trace* trans trans! trans-eval trans-eval-default-warning trans-eval-no-warning trans1 translam translate-and-test trichotomy true-list-fix true-list-listp true-list-listp-forward-to-true-listp true-list-listp-forward-to-true-listp-assoc-equal true-listp true-listp-cadr-assoc-eq-for-open-channels-p true-listp-update-nth truncate trust-mfc ttag ttags-seen tthm type typed-io-listp typed-io-listp-forward-to-true-listp typespec-check u ubt ubt! ubt-prehistory ubt? ubu ubu! ubu? unary-- unary-/ unary-function-symbol-listp unicity-of-0 unicity-of-1 union$ union-eq union-equal union-theories universal-theory unmemoize unmonitor unquote unsave unsigned-byte unsigned-byte-p until$ until$+ untouchable-marker untrace$ untrans-table untranslate update-acl2-oracle update-acl2-oracle-preserves-state-p1 update-big-clock-entry update-file-clock update-global-table update-idates update-nth update-nth-array update-open-input-channels update-open-output-channels update-read-files update-user-stobj-alist update-user-stobj-alist1 update-written-files upper-case-p upper-case-p-char-upcase upper-case-p-forward-to-alpha-char-p user-stobj-alist user-stobj-alist1 value value-cmp value-triple verbose-pstack verify verify-guard-implication verify-guards verify-guards+ verify-guards-formula verify-termination w walkabout warning! warrant waterfall-parallelism waterfall-printing weak-ld-history-entry-p well-formed-lambda-objectp wet when$ when$+ with-cbd with-fast-alist with-global-stobj with-guard-checking with-guard-checking-error-triple with-guard-checking-event with-live-state with-local-state with-local-stobj with-output with-output! with-output-lock with-prover-step-limit with-prover-step-limit! with-prover-time-limit with-serialize-character with-stolen-alist without-evisc wof world wormhole wormhole-data wormhole-entry-code wormhole-eval wormhole-p wormhole-statusp wormhole1 writable-file-listp writable-file-listp-forward-to-true-list-listp writable-file-listp1 writable-file-listp1-forward-to-true-listp-and-consp write-byte$ writeable-files writeable-files-p writeable-files-p-forward-to-writable-file-listp written-file written-file-forward-to-true-listp-and-consp written-file-listp written-file-listp-forward-to-true-list-listp-and-alistp written-files written-files-p written-files-p-forward-to-written-file-listp xargs xor xxxjoin zero zerop zip zp zpf)