|
|
|---|
|
|
|
|---|
When the executable-counterpart is enabled, forced hypotheses are attacked immediately
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