[Merged by Bors] - fix(data/{Finset,Multiset}): better line breaks in Repr #6333
Conversation
See the attached tests
Previously this gave `{[1, 2,\n 3], [4, 5, 6]}`, where the line break
would be within items rather than between items.
eric-wieser
added
awaiting-review
eric-wieser
changed the title
| #eval show Lean.MetaM Unit from guard <| | ||
| (repr (0 : Multiset (List ℕ)) |>.pretty 15) = "0" |
There was a problem hiding this comment.
These tests might be clearer with a simple #guard_msgs, rather than mentioning MetaM.
There was a problem hiding this comment.
I specifically want to use a narrow width, so would prefer to test equality.
Is there a better way to write simple assertions than what I do here?
There was a problem hiding this comment.
There are a handful of other tests in this style, so I'm going to leave it as is for now
bors merge
|
bors d+ |
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
removed
the
awaiting-review
See the attached tests
Previously this gave `{[1, 2,\n 3], [4, 5, 6]}`, where the line break would be within items rather than between items.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
See the attached tests
Previously this gave `{[1, 2,\n 3], [4, 5, 6]}`, where the line break would be within items rather than between items.
See the attached tests
Previously this gave
{[1, 2,\n 3], [4, 5, 6]}, where the line break would be within items rather than between items.