Major Section: ACL2-BUILT-INS
(Setenv$ str val), where str and val are strings, sets the
environment variable str to have value val, for subsequent read by
getenv$ (see getenv$), and returns nil. Or, if this operation is
not implemented for the host Common Lisp, an error will occur.
Example: (setenv$ "FOO" "BAR")
It may be surprising that setenv$ returns nil; indeed, it neither
takes nor returns the ACL2 state. The reason is that getenv$
takes responsibility for trafficking in state; it is defined in the
logic using the function read-acl2-oracle, which (again, in the logic)
does modify state, by popping an entry from its acl2-oracle field.
getenv$.
