Documented default-state-vars

books/system/doc/acl2-doc.lisp

@@ -99242,6 +99242,19 @@ arithmetic) for libraries of @(see books) for arithmetic reasoning.</p>")
  simplification may be done; to avoid that, use @('fcons-term') (``fast
  cons-term'').  Also see @('fcons-term*') below.</li>
 
+ <li>@('(default-state-vars state-p &key ...)'): Returns a record suitable as
+ an argument for some utilities that take the @(see world) as an argument but
+ not the @(see state), such as @('translate-cmp').  That record provides values
+ for certain state global variables (which are not stored in the world), such
+ as @('guard-checking-on') (which holds the @(see guard)-checking mode).  As
+ described below, @('default-state-vars') provides suitable defaults, which
+ however can be modified by supplying keyword arguments corresponding to
+ certain state globals, such as @(':guard-checking-on').  When the required
+ argument is @('t'), those defaults are the values of those state globals;
+ thus, @('t') is probably the right value to use for that argument when the
+ state is available in the calling context.  Otherwise, those defaults are the
+ values commonly found in those state globals.</li>
+
  <li>@('(defined-constant name w)'): If @('name') is @('t'), @('nil'), or
  defined using @(tsee defconst), return @('(quote val)') where @('val') is the
  value of @('name'); otherwise return @('nil').</li>
@@ -116604,6 +116617,7 @@ expand function call at the current subterm, without simplifying"
 (defpointer cons-count-bounded system-utilities)
 (defpointer cons-term system-utilities)
 (defpointer context ctx)
+(defpointer default-state-vars system-utilities)
 (defpointer default-verify-guards-eagerness set-verify-guards-eagerness)
 (defpointer defined-constant system-utilities)
 (defpointer delete-assoc-eq delete-assoc)