I often have multiple subgoals with similar proof structures, except for some intermediate steps: e.g.
foo; bar; baz and
quux; bar; baz. Is there a way to introduce "non-determinism" of the form
[foo; quux]; bar; baz? (Assume that
(foo || quux); bar; baz might not work because
foo could succeed in the second case but lead to an unsolvable goal.)
+ instead of
(foo + quux); bar; baz; fail? or maybe
solve [ (foo + quux); bar; baz ]
Wow that's awesome, I wish I had asked this way sooner... thanks!
Last updated: Jan 29 2023 at 06:02 UTC