When executing a proof method expression m, n
, failure of n
triggers backtracking, possibly resulting in m
picking a different proof. How can I achieve that failure of n
results in only n
and the proof methods before m
searching for alternative proofs, so that m
is not reconsidering it’s choice of proof?
Last updated: Dec 21 2024 at 12:33 UTC