Major Section: ACL2-BUILT-INS
(Setenv$ str val), where
val are strings, sets the
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
nil; indeed, it neither
takes nor returns the ACL2 state. The reason is that
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.