Siddharth
Siddharth
I don’t have the rest of the context here, but to handle negations, we use the fact that regular expressions are closed under complementation. On Fri, Aug 9, 2024, at...
Overall LGTM. I didn't take too close a look, but I trust you, and it seems like we're trying to figure out the precise modelling, so bikeshedding isn't worth it!
Closing as abandoned.
@alexkeizer thanks for thinking about this, I'm generally happy with this change in terms of API surface area. I don't quite understand: > Controlling which parts of the grammar are...
we need to figure out what to do with sorrys
Asked on Lean zulip about suppressing sorrys: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/suppress.20sorry.20warnings/near/437970722
@tobiasgrosser that's a good idea, would you mind making the change?
Right. This is the type of thing that wants us to write an ad-hoc proof procedure, which tries multiple styles of proof, since there’s no good “normal form” for all...
I do not have a good sense of the tradeoffs, and would prefer to refactor this after #191 has been merged — we can try it out and see how...
Closed by https://github.com/opencompl/ssa/issues/252, https://github.com/opencompl/ssa/pull/254