max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add blackboard bold characters

Browse source
This commit is contained in:
Wojciech Nawrocki 2021-12-06 18:05:16 -05:00 • committed by Leonardo de Moura
parent c57a664127
commit c97487fd65
1 changed files with 27 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
lean4-mode/lean4-input.el
View file

@ -525,6 +525,33 @@ order for the change to take effect."
("bb" . ("𝔹"))
("bsum" . ("⅀"))
("bbA" . ("𝔸"))
("bbB" . ("𝔹"))
("bbC" . ("ℂ"))
("bbD" . ("𝔻"))
("bbE" . ("𝔼"))
("bbF" . ("𝔽"))
("bbG" . ("𝔾"))
("bbH" . ("ℍ"))
("bbI" . ("𝕀"))
("bbJ" . ("𝕁"))
("bbK" . ("𝕂"))
("bbL" . ("𝕃"))
("bbM" . ("𝕄"))
("bbN" . ("ℕ"))
("bbO" . ("𝕆"))
("bbP" . ("ℙ"))
("bbQ" . ("ℚ"))
("bbR" . ("ℝ"))
("bbS" . ("𝕊"))
("bbT" . ("𝕋"))
("bbU" . ("𝕌"))
("bbV" . ("𝕍"))
("bbW" . ("𝕎"))
("bbX" . ("𝕏"))
("bbY" . ("𝕐"))
("bbZ" . ("ℤ"))
;; Blackboard bold numbers.
("b0" . ("𝟘"))