Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(tactic/observe): have a claim proved by library_search under the hood #10878

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(tactic/observe): have a claim proved by library_search under the hood #10878

wants to merge 5 commits into from

Conversation

jcommelin
Copy link
Member

Open in Gitpod

@jcommelin jcommelin added awaiting-review The author would like community review of the PR t-meta Tactics, attributes or user commands labels Dec 18, 2021
@sgouezel
Copy link
Collaborator

Can you add a test (importing as little as possible to make sure that the test is fast)?

@jcommelin @RemyDegenne
Update src/tactic/observe.lean
17ef882 
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
@ericrbg
Copy link
Collaborator

ericrbg commented Dec 18, 2021

also, should we put a linter to make sure this is never used in mathlib proper? otherwise it lgtm

@jcommelin
Copy link
Member Author

Good idea. Done.

robertylewis
robertylewis reviewed Dec 18, 2021
View reviewed changes
Copy link
Member

@robertylewis robertylewis left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seconding the request for tests, otherwise looks good!

src/tactic/observe.lean Outdated Show resolved Hide resolved
@robertylewis robertylewis added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Dec 18, 2021
@jcommelin @robertylewis
Update src/tactic/observe.lean
caecc1f 
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
@jcommelin jcommelin 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 Dec 18, 2021
@robertylewis
Copy link
Member

@jcommelin I think this is still awaiting-author for tests, right? Otherwise it's looking good.

@robertylewis robertylewis added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Dec 20, 2021
@jcommelin
Copy link
Member Author

Whoops, I thought I pushed a test, but I didn't push 🙈

@jcommelin jcommelin 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 Dec 20, 2021
@robertylewis
Copy link
Member

bors merge

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Dec 20, 2021
bors bot pushed a commit that referenced this pull request Dec 20, 2021
@jcommelin
feat(tactic/observe): have a claim proved by library_search under the…
b9fbef8 
… hood (#10878)
@github-actions github-actions bot removed the awaiting-review The author would like community review of the PR label Dec 20, 2021
@bors
Copy link

bors bot commented Dec 20, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(tactic/observe): have a claim proved by library_search under the hood [Merged by Bors] - feat(tactic/observe): have a claim proved by library_search under the hood Dec 20, 2021
@bors bors bot closed this Dec 20, 2021
@bors bors bot deleted the observe branch December 20, 2021 16:29
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@RemyDegenne RemyDegenne RemyDegenne left review comments

@robertylewis robertylewis robertylewis left review comments

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+`.) t-meta Tactics, attributes or user commands
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@jcommelin @sgouezel @ericrbg @robertylewis @RemyDegenne