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.)
There is +
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: Oct 13 2024 at 01:02 UTC