forced hypotheses are attacked immediately
Major Section: MISCELLANEOUS
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.
