Jetbrainsmono: Support for APL, Agda et al.

[takanuva]

Are there any plans to support symbols for programming in APL? Other languages, such as Agda, use a few unicode mathematical symbols for programming, and could benefit as well.

I have previously discussed this issue here, and it has been continued here for other fonts.

Disclaimer: I have written some APL code in the past, but it's been a long time since I've last done that. More recently I've written some Agda code, though.

[ice1000]

EDIT: updated the list.

Here's the top few unicode characters used in Agda's standard library:

Click to see, the list is long

→ (U+2192): 18506
₂ (U+2082): 8525
₁ (U+2081): 8329
≤ (U+2264): 7606
≡ (U+2261): 6826
≈ (U+2248): 6653
∀ (U+2200): 5829
∷ (U+2237): 5218
ℓ (U+2113): 4565
′ (U+2032): 3876
ℕ (U+2115): 3855
⟩ (U+27e9): 3622
⟨ (U+27e8): 3622
ʳ (U+2b3): 2944
⁺ (U+207a): 2666
⇒ (U+21d2): 2548
∣ (U+2223): 2403
ˡ (U+2e1): 2355
∼ (U+223c): 2319
∘ (U+2218): 2268
λ (U+3bb): 2191
ρ (U+3c1): 1907
∈ (U+2208): 1857
⊔ (U+2294): 1756
∧ (U+2227): 1588
× (U+d7): 1521
¬ (U+ac): 1511
∙ (U+2219): 1447
∨ (U+2228): 1438
⊆ (U+2286): 1401
⟧ (U+27e7): 1392
⟦ (U+27e6): 1392
⁻ (U+207b): 1245
ℤ (U+2124): 1124
≟ (U+225f): 1055
≢ (U+2262): 1014
⊎ (U+228e): 886
∸ (U+2238): 882
⊥ (U+22a5): 861
∎ (U+220e): 830
↔ (U+2194): 778
₃ (U+2083): 747
⊓ (U+2293): 708
⊤ (U+22a4): 706
↭ (U+21ad): 647
ₚ (U+209a): 573
⟶ (U+27f6): 570
τ (U+3c4): 554
ℚ (U+211a): 553
ᴹ (U+1d39): 539
≋ (U+224b): 528
↧ (U+21a7): 522
ᵘ (U+1d58): 462
≅ (U+2245): 452
ₗ (U+2097): 449
∃ (U+2203): 428
↥ (U+21a5): 428
ₙ (U+2099): 425
¹ (U+b9): 417
ᵣ (U+1d63): 407
≥ (U+2265): 389
₋ (U+208b): 381
⇔ (U+21d4): 364
ε (U+3b5): 364
⊕ (U+2295): 361
↑ (U+2191): 342
ᵇ (U+1d47): 340
∩ (U+2229): 335
≗ (U+2257): 309
≃ (U+2243): 303
ₕ (U+2095): 302
″ (U+2033): 287
∪ (U+222a): 272
≮ (U+226e): 265
⊖ (U+2296): 263
⊛ (U+229b): 262
Ρ (U+3a1): 252
± (U+b1): 243
ᵢ (U+1d62): 240
β (U+3b2): 234
≉ (U+2249): 227
◃ (U+25c3): 223
˘ (U+2d8): 220
⅀ (U+2140): 219
⋆ (U+22c6): 216
‿ (U+203f): 214
⇓ (U+21d3): 213
◅ (U+25c5): 206
≳ (U+2273): 202
δ (U+3b4): 199
σ (U+3c3): 194
Σ (U+3a3): 189
♭ (U+266d): 188
✶ (U+2736): 182
• (U+2022): 181
◦ (U+25e6): 177
◇ (U+25c7): 177
⇨ (U+21e8): 176
∞ (U+221e): 175
≰ (U+2270): 167
⌋ (U+230b): 160
⌊ (U+230a): 160
⊢ (U+22a2): 157
↠ (U+21a0): 156
₄ (U+2084): 155
⊙ (U+2299): 154
ₛ (U+209b): 154
∅ (U+2205): 149
∉ (U+2209): 148
⊐ (U+2290): 146
⊠ (U+22a0): 143
Δ (U+394): 139
π (U+3c0): 135
ⁿ (U+207f): 132
⊞ (U+229e): 127
↓ (U+2193): 127
⊂ (U+2282): 126
≺ (U+227a): 125
♯ (U+266f): 124
↣ (U+21a3): 123
≯ (U+226f): 122
Γ (U+393): 107
□ (U+25a1): 105
⟫ (U+27eb): 104
⟪ (U+27ea): 104
∹ (U+2239): 102
⋎ (U+22ce): 97
ₜ (U+209c): 93
∁ (U+2201): 91
↞ (U+219e): 91
  (U+a0): 89
≲ (U+2272): 86
‴ (U+2034): 86
⊑ (U+2291): 82
² (U+b2): 79
Κ (U+39a): 73
⋯ (U+22ef): 72
₀ (U+2080): 70
─ (U+2500): 68
⊸ (U+22b8): 67
γ (U+3b3): 67
≔ (U+2254): 64
← (U+2190): 63
Π (U+3a0): 63
ᴸ (U+1d38): 58
⊗ (U+2297): 56
∋ (U+220b): 56
³ (U+b3): 55
≼ (U+227c): 51
∑ (U+2211): 51
▻ (U+25bb): 50
⌉ (U+2309): 50
⌈ (U+2308): 50
≱ (U+2271): 47
ᵤ (U+1d64): 47
⇉ (U+21c9): 46
— (U+2014): 44
⨀ (U+2a00): 43
ₑ (U+2091): 43
⊡ (U+22a1): 42
≫ (U+226b): 42
∶ (U+2236): 41
₅ (U+2085): 41
≠ (U+2260): 39
̇ (U+307): 38
↦ (U+21a6): 37
⁆ (U+2046): 37
⁅ (U+2045): 37
⟆ (U+27c6): 36
⟅ (U+27c5): 36
≪ (U+226a): 35
ₓ (U+2093): 35
· (U+b7): 34
▷ (U+25b7): 33
ᵐ (U+1d50): 33
│ (U+2502): 30
ᵒ (U+1d52): 30
ʸ (U+2b8): 30
é (U+e9): 29
⇑ (U+21d1): 27
ᴬ (U+1d2c): 26
⤖ (U+2916): 25
↪ (U+21aa): 25
↩ (U+21a9): 25
⊟ (U+229f): 24
ⱼ (U+2c7c): 23
⨆ (U+2a06): 23
₆ (U+2086): 22
ᵈ (U+1d48): 22
ʰ (U+2b0): 22
║ (U+2551): 20
ᴮ (U+1d2e): 20
⍓ (U+2353): 19
⊈ (U+2288): 19
ι (U+3b9): 19
⋐ (U+22d0): 18
⊇ (U+2287): 18
ₐ (U+2090): 18
⦈ (U+2988): 17
⦇ (U+2987): 17
◂ (U+25c2): 17
ƛ (U+19b): 17
ϕ (U+3d5): 16
κ (U+3ba): 16
⋃ (U+22c3): 15
↢ (U+21a2): 15
⋂ (U+22c2): 14
↾ (U+21be): 14
↝ (U+219d): 14
Ι (U+399): 14
𝕊 (U+1d54a): 13
⊜ (U+229c): 13
; (U+37e): 13
⇐ (U+21d0): 12
ₖ (U+2096): 12
₇ (U+2087): 12
₊ (U+208a): 11
⊝ (U+229d): 10
∄ (U+2204): 10
η (U+3b7): 10
½ (U+bd): 10
⊉ (U+2289): 9
⊄ (U+2284): 9
∤ (U+2224): 9
φ (U+3c6): 9
ˢ (U+2e2): 9
⊴ (U+22b4): 8
⊃ (U+2283): 8
… (U+2026): 8
ᵉ (U+1d49): 8
ᵀ (U+1d40): 8
ᴿ (U+1d3f): 8
÷ (U+f7): 7
◈ (U+25c8): 6
═ (U+2550): 6
⊒ (U+2292): 6
⊅ (U+2285): 6
μ (U+3bc): 6
⨅ (U+2a05): 5
└ (U+2514): 5
≻ (U+227b): 5
≬ (U+226c): 5
₉ (U+2089): 5
₈ (U+2088): 5
｝ (U+ff5d): 4
｛ (U+ff5b): 4
╲ (U+2572): 4
╱ (U+2571): 4
┘ (U+2518): 4
↗ (U+2197): 4
‼ (U+203c): 4
ᵥ (U+1d65): 4
ν (U+3bd): 4
α (U+3b1): 4
̄ (U+304): 4
𝔽 (U+1d53d): 3
⋢ (U+22e2): 3
⋊ (U+22ca): 3
⋉ (U+22c9): 3
⊘ (U+2298): 3
≇ (U+2247): 3
⇛ (U+21db): 3
ₘ (U+2098): 3
ᶜ (U+1d9c): 3
ψ (U+3c8): 3

[philippnurullin]

@takanuva I think we will get there, in time. )