Testing-enabled
Testing enable/disable flag
Testing can be enabled or disabled using this parameter.
The default value is :naive (unless you are in the usual
ACL2 Sedan session modes, where default is t). Setting this
parameter to nil amounts to disabling the testing
mechanism. Setting this parameter to :on-failure is similar to
setting it to t, except for some undocumented behavior related
to redefined versions of defthm. Setting this parameter to
:naive leads to top-level testing without any theorem
prover support.
Usage:
(acl2s-defaults :set testing-enabled :naive)
(acl2s-defaults :get testing-enabled)
:doc testing-enabled
