From 3b6599b12470fe9b1321111d31c34685ffd5db52 Mon Sep 17 00:00:00 2001 From: Marshall Lochbaum Date: Mon, 24 Jan 2022 18:12:13 -0500 Subject: Github doesn't remove Unicode letters from header slugs apparently --- docs/help/groupindices_group.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'docs/help/groupindices_group.html') diff --git a/docs/help/groupindices_group.html b/docs/help/groupindices_group.html index 55be5ee1..9c0742c1 100644 --- a/docs/help/groupindices_group.html +++ b/docs/help/groupindices_group.html @@ -5,7 +5,7 @@
(github) / BQN / help

Square Cup (⊔)

-

⊔ 𝕩: Group Indices

+

⊔ 𝕩: Group Indices

Group the indices of the major cells of 𝕩 by their respective values.

𝕩 must consist of integers. Groups start from 0.

↗️
       ⊔ 4‿5‿6‿6‿4‿7‿5
@@ -17,7 +17,7 @@
   ⟨⟩ ⟨⟩ ⟨⟩ ⟨⟩ ⟨ 0 4 ⟩ ⟨ 1 6 ⟩ ⟨ 2 3 ⟩ ⟨ 5 ⟩  
                                             ┘
-

𝕨 ⊔ 𝕩: Group

+

𝕨 ⊔ 𝕩: Group

Group the major cells of 𝕩 by their respective indices in 𝕨.

If an element corresponds to ¯1, it is excluded from grouping.

An extra element can be added to the end of 𝕨 to specify length of the result.

-- cgit v1.2.3