|
|
|---|
|
|
|
|---|
Add or delete an error output string from the
See set-inhibit-er for relevant background.
General Form: (toggle-inhibit-er string)
where
Note: This is an event! It does not print the usual event summary
but nevertheless changes the ACL2 logical world and is so recorded.
It is local to the book or encapsulate form in which it
occurs; see toggle-inhibit-er! for a corresponding non-local event. Indeed,
The given string is added to the list of strings used for inhibiting error
output if it is not there already and is deleted from the list if it is
there. Case is unimportant in