Skip to content

chore: fix Data.Bool to use _root_.decide_eq_true#566

Closed
pechersky wants to merge 4 commits intomasterfrom
pechersky/realign-bool-decide
Closed

chore: fix Data.Bool to use _root_.decide_eq_true#566
pechersky wants to merge 4 commits intomasterfrom
pechersky/realign-bool-decide

Conversation

@pechersky
Copy link
Copy Markdown
Contributor

@pechersky pechersky commented Nov 11, 2022 •
edited
Loading

by calling out to _root_
There was a clash between PRs

@pechersky
chore: fix Data.Bool
cca0b1b 
by calling out to root
There was a clash between PRs
@pechersky pechersky changed the title chore: fix Data.Bool chore: fix Data.Bool to use _root_.decide_eq_true Nov 11, 2022
@pechersky
Copy link
Copy Markdown
Contributor Author

pechersky commented Nov 11, 2022

Locally, this is causing make lint to complain -- not sure why both commits succeeded on CI, I would have thought the first would have failed.

@kbuzzard
Copy link
Copy Markdown
Member

kbuzzard commented Nov 11, 2022

This looks fine to me but I don't know about the lint issues.

@pechersky
Copy link
Copy Markdown
Contributor Author

pechersky commented Nov 11, 2022

make lint isn't so much about the linter, I use it as the most noisy lean builder

@pechersky pechersky mentioned this pull request Nov 11, 2022
Closed
2 tasks
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Nov 17, 2022

@pechersky, I'm confused, this PR has no effect: there's no Bool.decide_eq_true to disambiguate with.

@kim-em kim-em closed this Nov 17, 2022
bors bot pushed a commit that referenced this pull request Nov 18, 2022
@kim-em @pechersky @Vierkantor
feat: port Order.Max (#567)
e07097c 
mathlib3 hash: fd47bdf09e90f553519c712378e651975fe8c829

- [x] depends on: #566 
- [x] depends on: #562 



Co-authored-by: Yakov Pechersky <ypechersky@treeline.bio>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@int-y1 int-y1 deleted the pechersky/realign-bool-decide branch April 16, 2023 18:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@pechersky @kbuzzard @kim-em