Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - chore(logic/function/basic): remove classical decidable instance from a lemma statement #6488

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - chore(logic/function/basic): remove classical decidable instance from a lemma statement #6488

wants to merge 4 commits into from

Conversation

eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Mar 1, 2021 •
edited
Loading

Found using #6485

This means that this lemma can be use in reverse against any ite, not just one that uses classical.decidable.

@eric-wieser eric-wieser closed this Mar 1, 2021
@eric-wieser eric-wieser reopened this Mar 1, 2021
@bryangingechen bryangingechen added the awaiting-review The author would like community review of the PR label Mar 1, 2021
@semorrison
Copy link
Collaborator

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Mar 2, 2021
bors bot pushed a commit that referenced this pull request Mar 2, 2021
@eric-wieser
chore(logic/function/basic): remove classical decidable instance from…
5361162 
… a lemma statement (#6488)

Found using #6485

This means that this lemma can be use in reverse against any `ite`, not just one that uses `classical.decidable`.
@bors
Copy link

bors bot commented Mar 2, 2021

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Mar 2, 2021
@eric-wieser
chore(logic/function/basic): remove classical decidable instance from…
c5e1ad0 
… a lemma statement (#6488)

Found using #6485

This means that this lemma can be use in reverse against any `ite`, not just one that uses `classical.decidable`.
@bors
Copy link

bors bot commented Mar 2, 2021

Build failed (retrying...):

@bryangingechen
Copy link
Collaborator

Not sure why CI didn't run on this PR before, but it's failing now: https://github.com/leanprover-community/mathlib/runs/2009568932

logic/function/basic is apparently too early to use the convert tactic.

bors r-

@bors
Copy link

bors bot commented Mar 2, 2021

Canceled.

@bryangingechen bryangingechen added awaiting-author A reviewer has asked the author a question or requested changes and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Mar 2, 2021
@eric-wieser eric-wieser added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 6, 2021
@semorrison
Copy link
Collaborator

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Apr 6, 2021
bors bot pushed a commit that referenced this pull request Apr 7, 2021
@eric-wieser
chore(logic/function/basic): remove classical decidable instance from…
97832da 
… a lemma statement (#6488)

Found using #6485

This means that this lemma can be use in reverse against any `ite`, not just one that uses `classical.decidable`.
@bors
Copy link

bors bot commented Apr 7, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(logic/function/basic): remove classical decidable instance from a lemma statement [Merged by Bors] - chore(logic/function/basic): remove classical decidable instance from a lemma statement Apr 7, 2021
@bors bors bot closed this Apr 7, 2021
@bors bors bot deleted the eric-wieser/function.extend_def-decidable branch April 7, 2021 06:33
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@eric-wieser @semorrison @bryangingechen