IMMEDIATE-FORCE-MODEP

when executable counterpart is enabled, forced hypotheses are attacked immediately
Major Section:  MISCELLANEOUS

Also see disable-immediate-force-modep and see enable-immediate-force-modep.

This function symbol is defined simply to provide a rune which can be enabled and disabled. Enabling

(:executable-counterpart immediate-force-modep)
causes ACL2 to attack forced hypotheses immediately instead of delaying them to the next forcing round.
Example Hints
:in-theory (disable (:executable-counterpart immediate-force-modep))
           ; delay forced hyps to forcing round
:in-theory (enable (:executable-counterpart immediate-force-modep))
           ; split on forced hyps immediately

See force for background information. When a forced hypothesis cannot be established a record is made of that fact and the proof continues. When the proof succeeds a ``forcing round'' is undertaken in which the system attempts to prove each of the forced hypotheses explicitly. However, if the rune (:executable-counterpart immediate-force-modep) is enabled at the time the hypothesis is forced, then ACL2 does not delay the attempt to prove that hypothesis but undertakes the attempt more or less immediately.