kframework / matching-logic-prover

15 stars 4 forks source link

Deterministic choice operator #71

Open h0nzZik opened 4 years ago

h0nzZik commented 4 years ago

Implements https://github.com/kframework/matching-logic-prover/issues/63.

So far, only the strategy and-split uses it. I plan to use it in apply and apply-equation.