Skip to content

[Merged by Bors] - chore: Rename IsROrC to RCLike#10819

Closed
YaelDillies wants to merge 29 commits intomasterfrom
r_or_c_like
Closed

[Merged by Bors] - chore: Rename IsROrC to RCLike#10819
YaelDillies wants to merge 29 commits intomasterfrom
r_or_c_like

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Feb 21, 2024 •
edited by jcommelin
Loading

IsROrC contains data, which goes against the expectation that classes prefixed with Is are prop-valued. People have been complaining about this on and off, so this PR renames IsROrC to RCLike.

Open in Gitpod

@YaelDillies
chore: Rename IsROrC to ROrCLike
bf154a4 
`IsROrC` contains data, which goes against the expectation that classes prefixed with `Is` are prop-valued. People have been complaining about this on and off, so this PR renames `IsROrC` to `ROrCLike`.
@YaelDillies YaelDillies added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Feb 21, 2024
github-actions[bot]
github-actions bot reviewed Feb 21, 2024
View reviewed changes
@YaelDillies YaelDillies requested a review from kbuzzard February 21, 2024 15:47
YaelDillies and others added 4 commits February 21, 2024 16:49
@YaelDillies @github-actions
style
13ea15b 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@YaelDillies
break long lines
07a0db2
@YaelDillies
update Mathlib
c600cf2
@YaelDillies
fix Analysis.Complex.Basic
92da02e
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 21, 2024
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 23, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 23, 2024
@kbuzzard
Copy link
Copy Markdown
Member

kbuzzard commented Feb 23, 2024 •
edited
Loading

This is fine by me, although I have only recently understood the scope of the problem. Many properties of topological spaces (e.g. CompactSpace, QuasiSober, QuasiSeparatedSpace, T0Space, T2Space etc etc) are Props with no Is, plenty of other Props (e.g. Odd, Even) have no Is, and conversely there are a other non-Props with Is names like CategoryTheory.IsLeftAdjoint, CategoryTheory.IsRightAdjoint, CategoryTheory.IsEquivalence.

I've reopened the discussion here.

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 27, 2024
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Feb 27, 2024
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Feb 27, 2024
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Mar 2, 2024
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Mar 2, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 5, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 22, 2024
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 22, 2024
@YaelDillies YaelDillies changed the title chore: Rename IsROrC to ROrCLike chore: Rename IsROrC to RCLike Mar 22, 2024
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Mar 22, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 23, 2024
@fpvandoorn
Copy link
Copy Markdown
Member

fpvandoorn commented Mar 23, 2024

Given how much we already violate the meaning of the Is-prefix, I'm not entirely convinced by this change. The previous name was more descriptive for people using the class (LikeROrC also satisfies this property, if we want to remove the Is).
I'm not necessarily against this PR though, we (and new users) will get used to the new name.

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 23, 2024
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Mar 23, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 27, 2024
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Mar 28, 2024

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Mar 28, 2024
mathlib-bors bot pushed a commit that referenced this pull request Mar 28, 2024
@YaelDillies
chore: Rename IsROrC to RCLike (#10819)
43618f9 
`IsROrC` contains data, which goes against the expectation that classes prefixed with `Is` are prop-valued. People have been complaining about this on and off, so this PR renames `IsROrC` to `RCLike`.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 28, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: Rename IsROrC to RCLike [Merged by Bors] - chore: Rename IsROrC to RCLike Mar 28, 2024
@mathlib-bors mathlib-bors bot closed this Mar 28, 2024
@mathlib-bors mathlib-bors bot deleted the r_or_c_like branch March 28, 2024 11:36
xgenereux pushed a commit that referenced this pull request Apr 15, 2024
@YaelDillies @xgenereux
chore: Rename IsROrC to RCLike (#10819)
026d3d9 
`IsROrC` contains data, which goes against the expectation that classes prefixed with `Is` are prop-valued. People have been complaining about this on and off, so this PR renames `IsROrC` to `RCLike`.
atarnoam pushed a commit that referenced this pull request Apr 16, 2024
@YaelDillies @atarnoam
chore: Rename IsROrC to RCLike (#10819)
ce87d53 
`IsROrC` contains data, which goes against the expectation that classes prefixed with `Is` are prop-valued. People have been complaining about this on and off, so this PR renames `IsROrC` to `RCLike`.
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
@YaelDillies @uniwuni
chore: Rename IsROrC to RCLike (#10819)
e8fbf69 
`IsROrC` contains data, which goes against the expectation that classes prefixed with `Is` are prop-valued. People have been complaining about this on and off, so this PR renames `IsROrC` to `RCLike`.
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@YaelDillies @callesonne
chore: Rename IsROrC to RCLike (#10819)
7dc1627 
`IsROrC` contains data, which goes against the expectation that classes prefixed with `Is` are prop-valued. People have been complaining about this on and off, so this PR renames `IsROrC` to `RCLike`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@github-actions github-actions[bot] github-actions[bot] left review comments

@kbuzzard kbuzzard Awaiting requested review from kbuzzard

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@YaelDillies @kbuzzard @sgouezel @fpvandoorn @jcommelin