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.

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

chore(algebra/ring): use curly brackets for ring_hom where possible #1525

Merged
merged 7 commits into from
Oct 11, 2019

Conversation

ChrisHughes24
Copy link
Member

@ChrisHughes24 ChrisHughes24 commented Oct 9, 2019

TO CONTRIBUTORS:

Make sure you have:

  • reviewed and applied the coding style: coding, naming
  • reviewed and applied the documentation requirements
  • for tactics:
  • make sure definitions and lemmas are put in the right files
  • make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

@rwbarton
Copy link
Collaborator

rwbarton commented Oct 9, 2019

Let's try to document why we are doing this somewhere, because using implicit arguments like this is not an obvious choice. I suggest writing a Note

/- Note [instances as implicit arguments]
...  -- try to discuss what goes wrong with [] arguments, or why it leads to wasted effort by Lean in specific examples
-/

Specializing to ring or semiring is fine. Then we can also refer to the note in ring_theory.algebra or wherever else we want to make a similar change.

@ChrisHughes24 ChrisHughes24 added the awaiting-review The author would like community review of the PR label Oct 9, 2019
src/algebra/ring.lean Outdated Show resolved Hide resolved
src/algebra/ring.lean Outdated Show resolved Hide resolved
@jcommelin jcommelin 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 Oct 11, 2019
@mergify mergify bot merged commit 6b7377a into master Oct 11, 2019
@mergify mergify bot deleted the ring_hom_brackets branch October 11, 2019 13:15
anrddh pushed a commit to anrddh/mathlib that referenced this pull request May 15, 2020
…eanprover-community#1525)

* chore(algebra/ring): use curly brackets for ring_hom where possible

* add comments explaining motivation

* move explanation to header

* fix build

* Update src/algebra/ring.lean

* scott's suggestion
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
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
Development

Successfully merging this pull request may close these issues.

None yet

4 participants