Make mem_filter stronger #3200
Make mem_filter stronger #3200
Conversation
chandradeepdey
commented
Jan 30, 2024
•
chandradeepdey
commented
- Mirrors TSet
- Remove the refinement on the return type of filter, it was implied by the SMTPat on mem_filter_forall anyway
chandradeepdey
changed the title
- Mirrors TSet - Remove the refinement on the return type of filter, it was implied by the SMTPat on mem_filter_forall anyway
|
@aseemr Check this one please? |
|
Hi @chandradeepdey, thanks for the PR! I merged master into this branch and F* build fails. It could be some brittleness in the proofs. If we make F* work, I would also like to run our everest CI on it to make sure that we are not breaking any of the client code in everest. If something breaks there, we would have to fix that too. On the other hand, if you can make things work on your end using some wrappers or locally defined patterns, perhaps that's a quicker way to make progress. |
|
@aseemr Builds now!
I have it in my code already. Wanted to push it here so I could delete it from there 😅 |
|
Thanks! I started a local everest build on my machine. |
