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/scan.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'docs/help/scan.html') diff --git a/docs/help/scan.html b/docs/help/scan.html index c68b6fd2..464d9fa7 100644 --- a/docs/help/scan.html +++ b/docs/help/scan.html @@ -5,7 +5,7 @@

Grave (`)

-

𝔽` 𝕩: Scan

+

𝔽` 𝕩: Scan

Scan over 𝕩 with 𝔽 from left to right, producing intermediate values.

↗️
       +` 123
 ⟨ 1 3 6 ⟩
@@ -19,7 +19,7 @@
        1, 1-2, (1-2)-3
 ⟨ 1 ¯1 ¯4 ⟩
 
-

𝕨 𝔽` 𝕩: Scan With initial

+

𝕨 𝔽` 𝕩: Scan With initial

Monadic scan, but use 𝕨 as initial left argument.

↗️
       5 +` 123
 ⟨ 6 8 11 ⟩
-- 
cgit v1.2.3