diff options
| author | Marshall Lochbaum <mwlochbaum@gmail.com> | 2021-01-06 21:55:23 -0500 |
|---|---|---|
| committer | Marshall Lochbaum <mwlochbaum@gmail.com> | 2021-01-06 22:00:24 -0500 |
| commit | abe8ae4745bb2ebe3b71b047aa92e2ae89a414d5 (patch) | |
| tree | a9344b34a666ae7f83693762cb905db9f80e426e /doc/group.md | |
| parent | 337044f77dc491459e798625972cd83bed1e72bc (diff) | |
Avoid joining units in some documentation
Diffstat (limited to 'doc/group.md')
| -rw-r--r-- | doc/group.md | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/group.md b/doc/group.md index 592b868d..4bd82dc2 100644 --- a/doc/group.md +++ b/doc/group.md @@ -72,12 +72,12 @@ The obvious application of Group is to group some values according to a known or If we would like a particular index to key correspondence, we can use a fixed left argument to Index Of. countries ← "IT"‿"JP"‿"NO"‿"SU"‿"US" - countries ∾˘ co countries⊸⊐⊸⊔ ln + countries ≍˘ co countries⊸⊐⊸⊔ ln However, this solution will fail if there are trailing keys with no values. To force the result to have a particular length you can append that length as a dummy index to each argument, then remove the last group after grouping. countries ↩ "IT"‿"JP"‿"NO"‿"SU"‿"US"‿"ZW" - countries ∾˘ co countries{𝕗⊸⊐⊸(¯1↓⊔○(∾⟜(≠𝕗)))} ln + countries ≍˘ co countries{𝕗⊸⊐⊸(¯1↓⊔○(∾⟜(≠𝕗)))} ln ### Partitioning |