Siddharth
Siddharth
LGTM, yoink it in. Maybe ask Kim if we can toss it into core :)
turns out the statement of `mask_split_left` (resp. `mask_split_right`) was stronger than necessary, and the theorem isn't about masks at all. For sanity, we prove variants where the symbols are treated...
@shigoel all comments resolved.
Yep, closing.
@austinletson thank you very much :) If you could add the line ```lean with: auto-config: false ``` to the PR, @shigoel can merge this in tomorrow ^_^
Thanks! @shigoel I think this is ready for "workflow approval"
LGTM, we paired on this, and I like the idea.
Superceded by #1444
Jesus, that's a chonky PR! I will hit "approve", but I would like us to think about the following questions: 1) How do we know that this faithfully implements Sail?...
Right. I feel it would be worth it to add Sail as a dependency, and the proofs of equivalence as a follow up PR @salinhkuhn. Let's see what @alexkeizer and...