		Search-engine friendly clone of the ACL2 documentation.

Std/system

A library that complements the built-in system utilities with theorems and with non-built-in system utilities.

This is just a start towards a comprehensive library. Some candidate utilities are under community-book kestrel/std.

Subtopics

Fresh-logical-name-with-$s-suffix: Suffix a name with as many $ signs as needed to make it a valid new logical name that is also not among a given list of names to avoid.
Irrelevant-formals-info: Determine whether irrelevant-formals are OK in definitions.
Std/system/function-queries: Utilities to query functions.
Std/system/term-queries: Utilities to query terms.
Std/system/term-transformations: Utilities to transform terms.
Std/system/enhanced-utilities: System utilities with some enhanced features.
Install-not-normalized-event-lst: Create a list of event forms to install the non-normalized definitions of a list of functions, ensuring that the names of the theorems will not cause a conflict.
Install-not-normalized-event: Create an event form to install the non-normalized definition of a function, ensuring that the name of the theorem will not cause a conflict.
Std/system/term-function-recognizers: Recognizers of functions in terms.
Pseudo-tests-and-call-listp: Recognize true lists of well-formed tests-and-call records.
Genvar$: A logic-mode guard-verified version of genvar.
Std/system/event-name-queries: Utilities to query names of events in the world.
Maybe-pseudo-event-formp: Recognize pseudo-event-formp values and nil.
Add-suffix-to-fn-or-const: Add a suffix to a function or constant name.
Chk-irrelevant-formals-ok: Check irrelevant-formals in definitions.
Std/system/good-atom-listp: Theorems about good-atom-listp.
Pseudo-tests-and-callp: Recognize well-formed tests-and-call records.
Table-alist+: Enhanced variant of table-alist.
Add-suffix-to-fn-or-const-lst: Apply add-suffix-to-fn-or-const to a list of symbols, all with the same suffix.
Known-packages+: Enhanced variant of known-packages.
Add-suffix-to-fn-lst: Apply add-suffix-to-fn to a list of symbols, all with the same suffix.
Unquote-term: Unquote a term that is a quoted constant.
Event-landmark-names: Names introduced by an event landmark.
Add-suffix-lst: Apply add-suffix to a list of symbols, all with the same suffix.
Std/system/theorem-queries: Utilities to query theorems.
Unquote-term-list: Lift unquote-term to lists.
Std/system/macro-queries: Utilities to query macros.
Pseudo-event-landmark-listp: Recognize true lists of event landmarks.
Pseudo-command-landmark-listp: Recognize true lists of command landmarks.
Install-not-normalized$: Install the non-normalized definition of a function, ensuring that the name of the theorem will not cause a conflict.
Rune-disabledp: Check if a rune is disabled.
Known-packages: List of names of the known packages, in chronological order.
Std/system/partition-rest-and-keyword-args: Theorems about partition-rest-and-keyword-args.
Rune-enabledp: Check if a rune is enabled.
Included-books: List of full pathnames of all books currently included (directly or indirectly).
Std/system/pseudo-event-formp: Theorems about pseudo-event-formp.
Std/system/plist-worldp-with-formals: Theorems about plist-worldp-with-formals (see the ACL2 source code).
Std/system/w: Theorems about w.
Std/system/geprops: Theorems about getprops (see the ACL2 source code).
Std/system/arglistp: Theorems about arglistp.
Std/system-extensions: Extensions of Std/system in the Kestrel Books.
Std/system/constant-queries: Utilities to query constants.