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(*): change notation for set.compl #3212

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - chore(*): change notation for set.compl #3212

wants to merge 8 commits into from

Conversation

urkud
Copy link
Member

@urkud urkud commented Jun 28, 2020 •
edited

  • introduce typeclass has_compl and notation sᶜ for compl s;
  • use it instead of has_neg for set and boolean_algebra

This way we'll be able to turn pointwise operations into instances.

@bryangingechen bryangingechen added the awaiting-review The author would like community review of the PR label Jun 28, 2020
@fpvandoorn
Copy link
Member

How about a postfix notation ᶜ (superscript c) for complement?

@fpvandoorn fpvandoorn mentioned this pull request Jun 29, 2020
Closed
bors bot pushed a commit to leanprover-community/lean that referenced this pull request Jun 29, 2020
@fpvandoorn
feat(data/set): remove has_neg instance (#367)
bdddb70 
See leanprover-community/mathlib#3212
@fpvandoorn
Copy link
Member

Looking good! You even went through the effort removing parentheses where possible :)

bors d+

@bors
Copy link

bors bot commented Jun 29, 2020

✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@fpvandoorn
Copy link
Member

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 Jun 29, 2020
bors bot pushed a commit that referenced this pull request Jun 29, 2020
@urkud
chore(*): change notation for set.compl (#3212)
45904fb 
* introduce typeclass `has_compl` and notation `∁` for `has_compl.compl`
* use it instead of `has_neg` for `set` and `boolean_algebra`
@fpvandoorn
Copy link
Member

immediately afterwards I noticed that the commit message wasn't quite right anymore. Oh well...

@urkud
Copy link
Member Author

urkud commented Jun 29, 2020

It's already running in bors but I fixed description anyway.

@bors
Copy link

bors bot commented Jun 29, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(*): change notation for set.compl [Merged by Bors] - chore(*): change notation for set.compl Jun 29, 2020
@bors bors bot closed this Jun 29, 2020
@bors bors bot deleted the set-compl branch June 29, 2020 20:22
@dwrensha dwrensha mentioned this pull request Feb 20, 2021
Merged
cipher1024 pushed a commit to cipher1024/mathlib that referenced this pull request Mar 15, 2022
@urkud @cipher1024
chore(*): change notation for set.compl (leanprover-community#3212)
066fc07 
* introduce typeclass `has_compl` and notation `∁` for `has_compl.compl`
* use it instead of `has_neg` for `set` and `boolean_algebra`
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@bryangingechen bryangingechen bryangingechen 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+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@urkud @fpvandoorn @bryangingechen