From 9f0bc9bdb8af4980516a710da4740eaecb8ee75d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 25 May 2026 11:11:50 +0000 Subject: [PATCH] =?UTF-8?q?feat:=20add=20abbreviations=20for=20heavy=20ang?= =?UTF-8?q?le=20brackets=20=E2=9D=B0=E2=9D=B1?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `h<` → ❰, `h>` → ❱, `h<>` → ❰$CURSOR❱, following the existing `f<`/`f>`/`f<>` pattern for French/single-arrow brackets `‹›`. The "h" prefix matches the Unicode names HEAVY LEFT/RIGHT- POINTING ANGLE BRACKET ORNAMENT (U+2770, U+2771). These characters are used by batteries' `proof_wanted` and `construction_wanted` commands (https://github.com/leanprover-community/batteries/pull/1814) as a bracket syntax for referencing earlier wanted declarations. Co-Authored-By: Claude Opus 4.7 (1M context) --- lean4-unicode-input/src/abbreviations.json | 3 +++ 1 file changed, 3 insertions(+) diff --git a/lean4-unicode-input/src/abbreviations.json b/lean4-unicode-input/src/abbreviations.json index dcf7a5c3..abe87c9b 100644 --- a/lean4-unicode-input/src/abbreviations.json +++ b/lean4-unicode-input/src/abbreviations.json @@ -14,6 +14,7 @@ "(())": "⸨$CURSOR⸩", "f<>": "‹$CURSOR›", "f<<>>": "«$CURSOR»", + "h<>": "❰$CURSOR❱", "[--]": "⁅$CURSOR⁆", "||||": "‖$CURSOR‖", "nnnorm": "‖$CURSOR‖₊", @@ -1163,6 +1164,8 @@ "f>>": "»", "f<": "‹", "f>": "›", + "h<": "❰", + "h>": "❱", "finprod": "∏ᶠ", "finsum": "∑ᶠ", "frac12": "½",