Major Section: MISCELLANEOUS
General Form: ACL2 !>:disable-forcing ; disallow forced case splitsSee force for a discussion of forced case splits.
Disable-forcing is a macro that disables the executable
counterpart of the function symbol
force; see force. When
you want to disable forcing in hints, use a form such as:
:in-theory (disable (:executable-counterpart force))