Stream: General

Topic: Preventing backtracking


view this post on Zulip Wolfgang Jeltsch (Nov 08 2021 at 12:57):

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 msearching for alternative proofs, so that m is not reconsidering it’s choice of proof?


Last updated: Apr 25 2024 at 16:19 UTC