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] - feat(set/basic): some results about set.pi #3894

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - feat(set/basic): some results about set.pi #3894

wants to merge 4 commits into from

Conversation

fpvandoorn
Copy link
Member

New definition: function.eval
Also some changes in set.basic
Name changes:

pi_empty_index -> empty_pi
pi_insert_index -> insert_pi
pi_singleton_index -> singleton_pi
set.push_pull -> image_inter_preimage
set.push_pull' -> image_preimage_inter

@fpvandoorn
feat(set/basic): some results about set.pi
ff484bb 
Name changes:
```
pi_empty_index -> empty_pi
pi_insert_index -> insert_pi
pi_singleton_index -> singleton_pi
set.push_pull -> image_inter_preimage
set.push_pull' -> image_preimage_inter
```
@fpvandoorn
fix
d077ec9
@fpvandoorn
undo part of fix
8ad980f
@fpvandoorn fpvandoorn added the awaiting-review The author would like community review of the PR label Aug 21, 2020
jcommelin
jcommelin approved these changes Aug 21, 2020
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

lgtm

Vierkantor
Vierkantor requested changes Aug 21, 2020
View reviewed changes
src/data/set/basic.lean Outdated Show resolved Hide resolved
src/logic/function/basic.lean Outdated Show resolved Hide resolved
@Vierkantor Vierkantor 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 Aug 21, 2020
@fpvandoorn @Vierkantor
Apply suggestions from code review
0900963 
Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
@fpvandoorn fpvandoorn 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 Aug 21, 2020
Vierkantor
Vierkantor approved these changes Aug 21, 2020
View reviewed changes
Copy link
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

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

Thanks!

bors r+

@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 Aug 21, 2020
bors bot pushed a commit that referenced this pull request Aug 21, 2020
@fpvandoorn
feat(set/basic): some results about set.pi (#3894)
1db32c5 
New definition: `function.eval`
Also some changes in `set.basic`
Name changes:
```
pi_empty_index -> empty_pi
pi_insert_index -> insert_pi
pi_singleton_index -> singleton_pi
set.push_pull -> image_inter_preimage
set.push_pull' -> image_preimage_inter
```
@bors
Copy link

bors bot commented Aug 21, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(set/basic): some results about set.pi [Merged by Bors] - feat(set/basic): some results about set.pi Aug 21, 2020
@bors bors bot closed this Aug 21, 2020
@bors bors bot deleted the set_pi branch August 21, 2020 20:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Vierkantor Vierkantor Vierkantor approved these changes

@jcommelin jcommelin jcommelin approved these changes

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
@fpvandoorn @Vierkantor @jcommelin