New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - refactor(logic/is_empty): tag is_empty.forall_iff
and is_empty.exists_iff
as simp
#14660
Conversation
forall_pempty
and exists_pempty
, mark forall_iff
and exists_iff
as simp
forall_iff
and exists_iff
as simp
forall_iff
and exists_iff
as simp
forall_iff
and exists_iff
as simp
This reverts commit ab640f8.
Is this your valuation or |
It's both my valuation and I'd give the extra justification for removing these lemmas that building much API on |
forall_iff
and exists_iff
as simp
is_empty.forall_iff
and is_empty.exists_iff
as simp
Looks good to me, thanks! Let's just have one last CI check before you merge. bors d=vihdzp |
✌️ vihdzp can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…sts_iff` as `simp` (#14660) We tag the lemmas `forall_iff` and `exists_iff` on empty types as `simp`. We remove `forall_pempty`, `exists_pempty`, `forall_false_left`, and `exists_false_left` due to being redundant.
Pull request successfully merged into master. Build succeeded: |
is_empty.forall_iff
and is_empty.exists_iff
as simp
is_empty.forall_iff
and is_empty.exists_iff
as simp
…sts_iff` as `simp` (#14660) We tag the lemmas `forall_iff` and `exists_iff` on empty types as `simp`. We remove `forall_pempty`, `exists_pempty`, `forall_false_left`, and `exists_false_left` due to being redundant.
We tag the lemmas
forall_iff
andexists_iff
on empty types assimp
. We removeforall_pempty
,exists_pempty
,forall_false_left
, andexists_false_left
due to being redundant.