[Merged by Bors] - fix: improve line-wrapping of (D)Finsupp reprs#17882
[Merged by Bors] - fix: improve line-wrapping of (D)Finsupp reprs#17882eric-wieser wants to merge 2 commits intomasterfrom
Conversation
Also update tests to use guard_msgs more effectively.
PR summary 54230edc2eImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for |
test/dfinsupp_notation.lean
Outdated
| /-- | ||
| info: | ||
| -/ | ||
| /-- info: (DFinsupp.single 1 3).update 2 3 : Π₀ (i : ℕ), Fin (i + 10) -/ |
There was a problem hiding this comment.
Why did this get broken? Before it would say fun₀ | 1 => 3 | 2 => 3.
There was a problem hiding this comment.
Ah, I accidentally replaced eval with check. I guess check was already broken.
test/finsupp_notation.lean
Outdated
| | ["there are five words here", "and five more words here"] => 5 | ||
| | ["there are seven words but only here"] => 7 | ||
| | ["just two"] => 2 |
There was a problem hiding this comment.
Indentation doesn't match between the #eval and the #check command, can you fix that?
There was a problem hiding this comment.
Which version do you prefer?
There was a problem hiding this comment.
I suppose the two-space-indented version is a bit clearer, but either works for me.
These were previously wrapping very poorly. Also update tests to use `#guard_msgs` more effectively, and fix a typo in the delaborators for DFinsupp.
|
Pull request successfully merged into master. Build succeeded: |
These were previously wrapping very poorly.
Also update tests to use
#guard_msgsmore effectively, and fix a typo in the delaborators for DFinsupp.