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

fix(data/encodable): make decidable_eq_of_encodable priority 0 #22

Closed
wants to merge 3 commits into from
Closed

fix(data/encodable): make decidable_eq_of_encodable priority 0 #22

wants to merge 3 commits into from

Conversation

kbuzzard
Copy link
Member

@kbuzzard kbuzzard commented Dec 4, 2017

Should I also add some unit test or something?

@johoelzl
Copy link
Collaborator

johoelzl commented Dec 4, 2017

I don't think a unit test is necessary, we generally don't have them in mathlib. But I would like to see a comment why priority 0 it is required. In a couple of weeks nobody will remember its reason.

@kbuzzard
Copy link
Member Author

kbuzzard commented Dec 6, 2017

Sorry this took forever. [I must be honest -- when I realised real mathlib had more commits than my fork I used this as an excuse to learn about git in general (clone, fork, merge, rebase, managing master + origin/master + remote/master)]. I added a comment.

[added later] Hmm. So did I not have to merge my suggested edit with mathlib in its current state?

@johoelzl
Copy link
Collaborator

This is now in the repo.

Sorry for the delay!

@johoelzl johoelzl closed this Dec 14, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants