Skip to content

[Merged by Bors] - refactor: change the way to_additive parses options#1780

Closed
fpvandoorn wants to merge 11 commits intomasterfrom
toadditivechangeoptions
Closed

[Merged by Bors] - refactor: change the way to_additive parses options#1780
fpvandoorn wants to merge 11 commits intomasterfrom
toadditivechangeoptions

Conversation

@fpvandoorn
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn commented Jan 23, 2023 •
edited
Loading

  • This is cleaner, and more scalable if we add more options
  • Related discussion on Zulip here

Open in Gitpod

@fpvandoorn fpvandoorn added awaiting-review t-meta Tactics, attributes or user commands awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jan 23, 2023
@fpvandoorn fpvandoorn removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jan 24, 2023
@fpvandoorn fpvandoorn mentioned this pull request Jan 27, 2023
Closed
2 tasks
@kim-em kim-em 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 1, 2023
@kim-em kim-em 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 3, 2023
@gebner
Copy link
Copy Markdown
Member

gebner commented Feb 3, 2023

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Feb 3, 2023
@bors
Copy link
Copy Markdown

bors bot commented Feb 3, 2023

Canceled.

@gebner
Copy link
Copy Markdown
Member

gebner commented Feb 3, 2023

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Feb 3, 2023

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

@github-actions github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 3, 2023
@fpvandoorn
Copy link
Copy Markdown
Member Author

fpvandoorn commented Feb 3, 2023

bors merge

bors bot pushed a commit that referenced this pull request Feb 3, 2023
@fpvandoorn
refactor: change the way to_additive parses options (#1780)
a33c403 
* This is cleaner, and more scalable if we add more options
* Related discussion on Zulip [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/syntax.20matches.20when.20literal.20doesn't)
@bors
Copy link
Copy Markdown

bors bot commented Feb 3, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor: change the way to_additive parses options [Merged by Bors] - refactor: change the way to_additive parses options Feb 3, 2023
@bors bors bot closed this Feb 3, 2023
@bors bors bot deleted the toadditivechangeoptions branch February 3, 2023 23:53
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

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-meta Tactics, attributes or user commands

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@fpvandoorn @gebner @kim-em