[Merged by Bors] - chore(data/multiset/sort): make multiset repr a meta instance #18163

ChrisHughes24 · 2023-01-13T11:38:49Z

Replaces #18075

…ports

jcommelin

Thanks 🎉

If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.

bors d+

bors · 2023-01-13T11:50:21Z

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

src/data/list/cycle.lean

src/data/multiset/sort.lean

src/data/pnat/factors.lean

Co-authored-by: Eric Wieser <[email protected]>

src/data/list/cycle.lean

eric-wieser · 2023-01-13T14:10:26Z

Just realised #eval does not look for meta instances of repr so none of this works

Yes it does?

#eval ({"this", "is", "fine"} : multiset string)
-- {"this", "is", "fine"}

…mmunity/mathlib into multiset-repr-meta

eric-wieser · 2023-01-13T14:15:50Z

I think the meta instance was probably more reasonable; can you revert 4c98928 and 60c1bd6

eric-wieser · 2023-01-13T14:16:30Z

bors d-

(since the PR has changed entirely)

This reverts commit 4c98928.

src/data/multiset/sort.lean

eric-wieser

bors d+

Looks like we're back where we were a few commits ago. Don't forget to change the PR title back too!

bors · 2023-01-13T14:28:42Z

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

Co-authored-by: Eric Wieser <[email protected]>

ChrisHughes24 · 2023-01-13T17:34:32Z

bors r+

bors · 2023-01-13T17:34:36Z

👎 Rejected by label

test/cycle.lean

ChrisHughes24 · 2023-01-13T20:32:31Z

bors merge

Co-authored-by: Chris Hughes <[email protected]> Co-authored-by: Eric Wieser <[email protected]>

bors · 2023-01-13T22:32:30Z

Build failed (retrying...):

Lint mathlib

Co-authored-by: Chris Hughes <[email protected]> Co-authored-by: Eric Wieser <[email protected]>

bors · 2023-01-14T05:56:31Z

Pull request successfully merged into master.

Build succeeded:

ChrisHughes24 added 2 commits January 13, 2023 11:38

chore(data/multiset/sort): make has_repr a meta instance to reduce im…

b9b9140

…ports

fix build

21bd006

ChrisHughes24 added the awaiting-review The author would like community review of the PR label Jan 13, 2023

jcommelin approved these changes Jan 13, 2023

View reviewed changes

leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jan 13, 2023

fix build

a418384

eric-wieser reviewed Jan 13, 2023

View reviewed changes

src/data/list/cycle.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 13, 2023

View reviewed changes

src/data/multiset/sort.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 13, 2023

View reviewed changes

src/data/pnat/factors.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 13, 2023

View reviewed changes

src/data/pnat/factors.lean Outdated Show resolved Hide resolved

ChrisHughes24 and others added 3 commits January 13, 2023 13:34

Update src/data/multiset/sort.lean

e218fdd

Co-authored-by: Eric Wieser <[email protected]>

Update src/data/pnat/factors.lean

38a0506

Co-authored-by: Eric Wieser <[email protected]>

Update src/data/pnat/factors.lean

7b323f2

Co-authored-by: Eric Wieser <[email protected]>

eric-wieser reviewed Jan 13, 2023

View reviewed changes

src/data/list/cycle.lean Outdated Show resolved Hide resolved

This was referenced Jan 13, 2023

Use a sensible sort order in multiset.repr #18166

Open

chore(data/multiset): move has_repr into its own file to remove data.string.basic import #18075

Closed

ChrisHughes24 added 2 commits January 13, 2023 14:13

make the instance non-meta again

4c98928

Merge branch 'multiset-repr-meta' of https://github.com/leanprover-co…

077459f

…mmunity/mathlib into multiset-repr-meta

revert changes to other files

60c1bd6

ChrisHughes24 changed the title ~~chore(data/multiset/sort): make has_repr a meta instance to reduce imports~~ chore(data/multiset/sort): fix multiset repr instance to not need string import Jan 13, 2023

eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes awaiting-CI The author would like to see what CI has to say before doing more work. and removed delegated The PR author may merge after reviewing final suggestions. labels Jan 13, 2023

ChrisHughes24 added 2 commits January 13, 2023 14:17

Revert "make the instance non-meta again"

afb48c2

This reverts commit 4c98928.

meta instance

1c303e1

ChrisHughes24 added 3 commits January 13, 2023 14:19

make finset instance meta

2c8201f

fix factors

f0ef658

fix cycle.lean

a1f4b21

eric-wieser reviewed Jan 13, 2023

View reviewed changes

src/data/multiset/sort.lean Show resolved Hide resolved

eric-wieser approved these changes Jan 13, 2023

View reviewed changes

leanprover-community-bot-assistant added the delegated The PR author may merge after reviewing final suggestions. label Jan 13, 2023

ChrisHughes24 changed the title ~~chore(data/multiset/sort): fix multiset repr instance to not need string import~~ chore(data/multiset/sort): make multiset repr a met instance Jan 13, 2023

ChrisHughes24 changed the title ~~chore(data/multiset/sort): make multiset repr a met instance~~ chore(data/multiset/sort): make multiset repr a meta instance Jan 13, 2023

ChrisHughes24 and others added 3 commits January 13, 2023 14:39

Update src/data/multiset/sort.lean

f9ada7d

Co-authored-by: Eric Wieser <[email protected]>

Update src/data/pnat/factors.lean

7ad390b

Co-authored-by: Eric Wieser <[email protected]>

fix

21358ee

github-actions bot 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-author A reviewer has asked the author a question or requested changes labels Jan 13, 2023

fix test

05db679

eric-wieser reviewed Jan 13, 2023

View reviewed changes

test/cycle.lean Outdated Show resolved Hide resolved

adjut test

a41d573

eric-wieser reviewed Jan 13, 2023

View reviewed changes

test/cycle.lean Outdated Show resolved Hide resolved

Update test/cycle.lean

c221d9e

github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jan 13, 2023

bors bot pushed a commit that referenced this pull request Jan 13, 2023

chore(data/multiset/sort): make multiset repr a meta instance (#18163)

44bb008

Co-authored-by: Chris Hughes <[email protected]> Co-authored-by: Eric Wieser <[email protected]>

bors bot pushed a commit that referenced this pull request Jan 14, 2023

chore(data/multiset/sort): make multiset repr a meta instance (#18163)

0063817

Co-authored-by: Chris Hughes <[email protected]> Co-authored-by: Eric Wieser <[email protected]>

bors bot changed the title ~~chore(data/multiset/sort): make multiset repr a meta instance~~ [Merged by Bors] - chore(data/multiset/sort): make multiset repr a meta instance Jan 14, 2023

bors bot closed this Jan 14, 2023

bors bot deleted the multiset-repr-meta branch January 14, 2023 05:56

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore(data/multiset/sort): make multiset repr a meta instance #18163

[Merged by Bors] - chore(data/multiset/sort): make multiset repr a meta instance #18163

ChrisHughes24 commented Jan 13, 2023 •

edited by eric-wieser

Loading

jcommelin left a comment

bors bot commented Jan 13, 2023

eric-wieser commented Jan 13, 2023 •

edited

Loading

eric-wieser commented Jan 13, 2023 •

edited

Loading

eric-wieser commented Jan 13, 2023 •

edited

Loading

eric-wieser left a comment

bors bot commented Jan 13, 2023

ChrisHughes24 commented Jan 13, 2023

bors bot commented Jan 13, 2023

ChrisHughes24 commented Jan 13, 2023

bors bot commented Jan 13, 2023

bors bot commented Jan 14, 2023

[Merged by Bors] - chore(data/multiset/sort): make multiset repr a meta instance #18163

[Merged by Bors] - chore(data/multiset/sort): make multiset repr a meta instance #18163

Conversation

ChrisHughes24 commented Jan 13, 2023 • edited by eric-wieser Loading

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Jan 13, 2023

eric-wieser commented Jan 13, 2023 • edited Loading

eric-wieser commented Jan 13, 2023 • edited Loading

eric-wieser commented Jan 13, 2023 • edited Loading

eric-wieser left a comment

Choose a reason for hiding this comment

bors bot commented Jan 13, 2023

ChrisHughes24 commented Jan 13, 2023

bors bot commented Jan 13, 2023

ChrisHughes24 commented Jan 13, 2023

bors bot commented Jan 13, 2023

bors bot commented Jan 14, 2023

ChrisHughes24 commented Jan 13, 2023 •

edited by eric-wieser

Loading

eric-wieser commented Jan 13, 2023 •

edited

Loading

eric-wieser commented Jan 13, 2023 •

edited

Loading

eric-wieser commented Jan 13, 2023 •

edited

Loading