STATE-GLOBAL-LET*

bind state global variables 
Major Section:  ACL2-BUILT-INS

See programming-with-state for requisite background on programming with the ACL2 state.

Example Forms:
(state-global-let*
 ((inhibit-output-lst *valid-output-names*))
 (thm (equal x x)))

(state-global-let*
 ((fmt-hard-right-margin 1000 set-fmt-hard-right-margin)
  (fmt-soft-right-margin 1000 set-fmt-soft-right-margin))
 (mini-proveall))

General Form:
(state-global-let* ((var1 form1) ; or (var1 form1 set-var1)
                    ...
                    (vark formk) ; or (vark formk set-vark)
                   )
                   body)
where: each vari is a variable; each formi is an expression whose value is a single ordinary object (i.e. not multiple values, and not state or any other stobj); set-vari, if supplied, is a function with signature ((set-vari * state) => state); and body is an expression that evaluates to an error triple (see error-triples). Each formi is evaluated in order, starting with form1, and with each such binding the state global variable vari is bound to the value of formi, sequentially in the style of let*. More precisely, then meaning of this form is to set (in order) the global values of the indicated state global variables vari to the values of formi using f-put-global, execute body, restore the vari to their previous values (but see the discussion of setters below), and return the triple produced by body (with its state as modified by the restoration). The restoration is guaranteed even in the face of aborts. The ``bound'' variables may initially be unbound in state and restoration means to make them unbound again.

Still referring to the General Form above, let old-vali be the value of state global variable vari at the time vari is about to be assigned the value of formi. If set-vari is not supplied, then as suggested above, the following form is evaluated at the conclusion of the evaluation of the state-global-let* form, whether or not an error has occurred: (f-put-global 'vari 'old-vali state). However, if set-vari is supplied, then instead the form evaluated will be (set-vari 'old-vali state). This capability is particularly useful if vari is untouchable (see push-untouchable), since the above call of f-put-global is illegal.