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