kblayouts/kbtrans/agda_list.py

287 lines
40 KiB
Python
Raw Normal View History

2023-11-09 14:16:16 +01:00
import re
from typing import List, Tuple
extras: List[Tuple[str, str]] = [
("cat", "🐱"),
("cat2", "🐈"),
("pl", "🥺"),
("plea", "🥺"),
("pleading", "🥺"),
("fl", "😳"),
("flushed", "😳"),
("crab", "🦀"),
("crazy hamburger", "🍔"),
("oil from iraq", "🛢️"),
("bread from turkie", "🍞"),
("cake", "🍰"),
("gec", "🦎"),
("amongus", ""),
("enby", ""),
("enby1", ""),
("enby2", ""),
("enby3", ""),
("dot", "·"),
("bullet", ""),
("multiocularo", ""),
("pleadpoint", "🥺👉👈"),
("point", "👉👈"),
("inv", "⁻¹"),
]
def parse_source(x: str) -> List[Tuple[str, str]]:
out = []
singular = re.compile(r'!(\S+)\s+(\S)\s+')
for k, v in singular.findall(x):
if '\\' in k or ("{" in k and "}" in k):
continue
if ord(v) < 0xffff:
out.append((k, v))
return out
source = r"""
!   !FB !bR !BGh 𝛈 !MiA 𝐴 !"{I} Ï !c{h} ḩ !amalg ∐ !lambda λ !^\script g ᶢ
!% !FC !bS 𝕊 !BGi 𝛊 !MiB 𝐵 !"{O} Ö !c{k} ķ !aoint ∳ !langle ⟨ !^\turned a ᵄ
!+ !FD !bT 𝕋 !BGk 𝛋 !MiC 𝐶 !"{U} Ü !c{l} ļ !asymp ≍ !lfloor ⌊ !^\turned h ᶣ
!- ­ !FE !bU 𝕌 !BGl 𝛌 !MiD 𝐷 !"{W} Ẅ !c{n} ņ !begin 〖 !ltimes ⋉ !^\turned i ᵎ
!0 !FF !bV 𝕍 !BGm 𝛍 !MiE 𝐸 !"{X} Ẍ !c{r} ŗ !below ┬ !mapsto ↦ !^\turned m ᵚ
!@ !FG !bW 𝕎 !BGn 𝛎 !MiF 𝐹 !"{Y} Ÿ !c{s} ş !cdots ⋯ !models ⊧ !^\turned r ʴ
!C !FH !bX 𝕏 !BGo 𝛚 !MiG 𝐺 !"{a} ä !c{t} ţ !close ┤ !nVDash ⊯ !^\turned v ᶺ
!H ̋ !FI !bY 𝕐 !BGp 𝛙 !MiH 𝐻 !"{e} ë !d-u- ⇵ !coint ∲ !nVdash ⊮ !^\turned w ꭩ
!I !FJ !bZ !BGr 𝛒 !MiI 𝐼 !"{h} ḧ !d\.S Ṩ !colon ₡ !nequiv ≢ !^\turned y 𐞠
!L Ł !FK !ba 𝕒 !BGs 𝛔 !MiJ 𝐽 !"{i} ï !d\.s ṩ !dashv ⊣ !nsimeq ≄ !circledast ⊛
!O Ø !FL !bb 𝕓 !BGt 𝛕 !MiK 𝐾 !"{o} ö !d\=L Ḹ !dddot ⃛ !numero № !complement ∁
!P !FM !bc 𝕔 !BGu 𝛖 !MiL 𝐿 !"{t} ẗ !d\=R Ṝ !ddots ⋱ !nvDash ⊭ !curlywedge ⋏
!S § !FN !bd 𝕕 !BGx 𝛏 !MiM 𝑀 !"{u} ü !d\=l ḹ !delta δ !nvdash ⊬ !eqslantgtr ⋝
!^ ̂ !FO !be 𝕖 !BGz 𝛇 !MiN 𝑁 !"{w} ẅ !d\=r ṝ !doteq ≐ !oiiint ∰ !gtreqqless ⋛
!k ̨ !FP !bf 𝕗 !BPi 𝚷 !MiO 𝑂 !"{x} ẍ !ddag ‡ !equiv ≡ !ominus ⊖ !lessapprox ≲
!v ̌ !FQ !bg 𝕘 !Box !MiP 𝑃 !"{y} ÿ !def= ≝ !frac1 ⅟ !oslash ⊘ !lesseqqgtr ⋚
!x × !FR !bh 𝕙 !Bpi 𝛑 !MiQ 𝑄 !'\.S Ṥ !defs ≙ !frown ⌢ !otimes ⊗ !longmapsto ⟼
!| !FS !bi 𝕚 !Cap !MiR 𝑅 !'\.s ṥ !dong ₫ !gamma γ !permil ‰ !mathscr{I}
!!! !FT !bj 𝕛 !Chi Χ !MiS 𝑆 !'\AE Ǽ !d{A} Ạ !gimel ℷ !peseta ₧ !nLeftarrow ⇍
!!? !FU !bk 𝕜 !Cup !MiT 𝑇 !'\ae ǽ !d{B} Ḅ !gneqq ≩ !pounds £ !nleftarrow ↚
!"' “ !FV !bl 𝕝 !Dei Ϯ !MiU 𝑈 !'{A} Á !d{D} Ḍ !gnsim ⋧ !pprime ″ !nsubseteqq ⊈
!"< « !FW !bm 𝕞 !Eta Η !MiV 𝑉 !'{C} Ć !d{E} Ẹ !iiint ∭ !preceq ≼ !nsupseteqq ⊉
!"> » !FX !bn 𝕟 !Fei Ϥ !MiW 𝑊 !'{E} É !d{H} Ḥ !imath ı !propto ∝ !precapprox ≾
!"A Ä !FY !bo 𝕠 !GTH Θ !MiX 𝑋 !'{G} Ǵ !d{I} Ị !infty ∞ !rangle ⟩ !prohibited 🛇
!"E Ë !FZ !bp 𝕡 !Gl- ƛ !MiY 𝑌 !'{I} Í !d{K} Ḳ !jmath ȷ !rddots ⋰ !registered ®
!"H Ḧ !Fa !bq 𝕢 !Glb ⨅ !MiZ 𝑍 !'{K} Ḱ !d{L} Ḷ !kappa κ !rfloor ⌋ !rightarrow →
!"I Ï !Fb !br 𝕣 !Gth θ !Mia 𝑎 !'{L} Ĺ !d{M} Ṃ !koppa ϟ !rtimes ⋊ !smallamalg ∐
!"O Ö !Fc !bs 𝕤 !H{} ˝ !Mib 𝑏 !'{M} Ḿ !d{N} Ṇ !lamda λ !square □ !smallsmile ⌣
!"U Ü !Fd !bt 𝕥 !Lsh ↰ !Mic 𝑐 !'{N} Ń !d{O} Ọ !lceil ⌈ !squb=n ⋢ !sqsubseteq ⊑
!"W Ẅ !Fe !bv 𝕧 !Lub ⨆ !Mid 𝑑 !'{O} Ó !d{R} Ṛ !ldata 《 !squp=n ⋣ !sqsupseteq ⊒
!"X Ẍ !Ff !bw 𝕨 !MCA 𝓐 !Mie 𝑒 !'{P} Ṕ !d{S} Ṣ !ldots … !stigma ϛ !subsetneqq ⊊
!"Y Ÿ !Fg !by 𝕪 !MCB 𝓑 !Mif 𝑓 !'{R} Ŕ !d{T} Ṭ !lneqq ≨ !subset ⊂ !succapprox ≿
!"` „ !Fh !bz 𝕫 !MCC 𝓒 !Mig 𝑔 !'{S} Ś !d{U} Ụ !lnsim ⋦ !succeq ≽ !supsetneqq ⊋
!"a ä !Fi !cC Ç !MCD 𝓓 !Mih !'{U} Ú !d{V} Ṿ !manat ₼ !supset ⊃ !textlquill ⁅
!"e ë !Fj !cD Ḑ !MCE 𝓔 !Mii 𝑖 !'{W} Ẃ !d{W} Ẉ !micro µ !textmu µ !textnumero №
!"h ḧ !Fk !cE Ȩ !MCF 𝓕 !Mij 𝑗 !'{Y} Ý !d{Y} Ỵ !minus !tugrik ₮ !textrecipe ℞
!"i ï !Fl !cG Ģ !MCG 𝓖 !Mik 𝑘 !'{Z} Ź !d{Z} Ẓ !nabla ∇ !u\'{A} Ắ !textrquill ⁆
!"o ö !Fm !cH Ḩ !MCH 𝓗 !Mil 𝑙 !'{a} á !d{a} ạ !naira ₦ !u\'{a} ắ !underbrace ⏟
!"t ẗ !Fn !cK Ķ !MCI 𝓘 !Mim 𝑚 !'{c} ć !d{b} ḅ !ncong ≇ !u\`{A} Ằ !underparen ⏝
!"u ü !Fo !cL Ļ !MCJ 𝓙 !Min 𝑛 !'{e} é !d{d} ḍ !ngeqq ≱ !u\`{a} ằ !upuparrows ⇈
!"w ẅ !Fp !cN Ņ !MCK 𝓚 !Mio 𝑜 !'{g} ǵ !d{e} ẹ !nleqq ≰ !u\d{A} Ặ !varepsilon ε
!"x ẍ !Fq !cR Ŗ !MCL 𝓛 !Mip 𝑝 !'{i} í !d{h} ḥ !nless ≮ !u\d{a} ặ !Rrightarrow ⇛
!"y ÿ !Fr !cS Ş !MCM 𝓜 !Miq 𝑞 !'{k} ḱ !d{i} ị !notin ∉ !u\~{A} Ẵ !Updownarrow ⇕
!'A Á !Fs !cT Ţ !MCN 𝓝 !Mir 𝑟 !'{l} ĺ !d{k} !nprec !u\~{a} !^\capital b 𐞄
!'C Ć !Ft !cc ç !MCO 𝓞 !Mis 𝑠 !'{m} ḿ !d{l} !nsucc !v\.{S} !^\capital g 𐞒
!'E É !Fu !cd ḑ !MCP 𝓟 !Mit 𝑡 !'{n} ń !d{m} !oiint !v\.{s} !^\capital h 𐞖
!'G Ǵ !Fv !ce ȩ !MCQ 𝓠 !Miu 𝑢 !'{o} ó !d{n} !omega ω !varkai ϗ !^\capital i
!'I Í !Fw !cg ģ !MCR 𝓡 !Miv 𝑣 !'{p} !d{o} !oplus !varphi φ !^\capital l
!'K Ḱ !Fx !ch ḩ !MCS 𝓢 !Miw 𝑤 !'{r} ŕ !d{r} !ounce !varrho ϱ !^\capital n
!'L Ĺ !Fy !ck ķ !MCT 𝓣 !Mix 𝑥 !'{s} ś !d{s} !pound £ !veebar !^\capital r 𐞪
!'M Ḿ !Fz !cn ņ !MCU 𝓤 !Miy 𝑦 !'{u} ú !d{t} !prcue !~\"{O} Ṏ !^\capital u ᶸ
!'N Ń !GA Α !cr ŗ !MCV 𝓥 !Miz 𝑧 !'{w} !d{u} !prime !~\"{o} ṏ !^\capital y 𐞲
!'O Ó !GB Β !cs ş !MCW 𝓦 !Psi Ψ !'{y} ý !d{v} ṿ !ratio !~\'{O} Ṍ !^\greek phi ᵠ
!'P Ṕ !GC Χ !ct ţ !MCX 𝓧 !Rho Ρ !'{z} ź !d{w} !rceil !~\'{U} Ṹ !^\rams horn 𐞑
!'R Ŕ !GD Δ !d- ↓ !MCY 𝓨 !Rsh ↱ !.\=A Ǡ !d{y} ỵ !rdata 》 !~\'{o} ṍ !^\turned ae ᵆ
!'S Ś !GE Ε !d= ⇓ !MCZ 𝓩 !San Ϻ !.\=O Ȱ !d{z} ẓ !rrect ▢ !~\'{u} ṹ !backepsilon ∍
!'U Ú !GF Φ !dd !MCa 𝓪 !Sho Ϸ !.\=a ǡ !euro € !ruble ₽ !~\={O} Ȭ !blacksmiley ☻
!'W Ẃ !GG Γ !dh ð !MCb 𝓫 !Tau Τ !.\=o ȱ !flat ♭ !rupee ₨ !~\={o} ȭ !blacksquare ▪
!'Y Ý !GH Η !dz ↯ !MCc 𝓬 !Yot Ϳ !.{A} Ȧ !flqq « !sampi ϡ !Diamond ◇ !circledcirc ⊚
!'Z Ź !GI Ι !ee !MCd 𝓭 !^Gb ᵝ !.{B} Ḃ !frqq » !sharp ♯ !Digamma Ϝ !circleddash ⊝
!'a á !GK Κ !em — !MCe 𝓮 !^Gc ᵡ !.{C} Ċ !geqq ≧ !shima ϭ !Epsilon Ε !curlyeqprec ⋞
!'c ć !GL Λ !en !MCf 𝓯 !^Gd ᵟ !.{D} Ḋ !gets ← !sigma σ !Omicron Ο !curlyeqsucc ⋟
!'e é !GM Μ !ex ∃ !MCg 𝓰 !^Ge ᵋ !.{E} Ė !glqq „ !simeq ≃ !Uparrow ⇑ !curlypreceq ≼
!'g ǵ !GN Ν !ge ≥ !MCh 𝓱 !^Gf ᵠ !.{F} Ḟ !gneq ≩ !smash ⬍ !Upsilon Υ !diamondsuit ♢
!'i í !GO Ω !gg ≫ !MCi 𝓲 !^Gg ᵞ !.{G} Ġ !grqq “ !smile ⌣ !^\alpha ᵅ !eqslantless ⋜
!'k ḱ !GP Ψ !ii !MCj 𝓳 !^a_ ª !.{H} Ḣ !hbar ℏ !sqcap ⊓ !^\delta ᵟ !nRightarrow ⇏
!'l ĺ !GR Ρ !in ∈ !MCk 𝓴 !^l- ⃖ !.{I} İ !heta ͱ !sqcup ⊔ !^\gamma ˠ !nrightarrow ↛
!'m ḿ !GS Σ !jj !MCl 𝓵 !^lr ⃡ !.{M} Ṁ !hori ϩ !squb= ⊑ !^\schwa ᵊ !ordfeminine ª
!'n ń !GT Τ !kA Ą !MCm 𝓶 !^o_ º !.{N} Ṅ !iint ∬ !squp= ⊒ !^\theta ᶿ !partnership ㉐
!'o ó !GU Υ !kE Ę !MCn 𝓷 !^r- ⃗ !.{O} Ȯ !iota ι !sub=n ⊈ !^\u bar ᶶ !precnapprox ⋨
!'p ṕ !GX Ξ !kI Į !MCo 𝓸 !_Gb ᵦ !.{P} Ṗ !k\=O Ǭ !sup=n ⊉ !afghani ؋ !radioactive ☢
!'r ŕ !GZ Ζ !kO Ǫ !MCp 𝓹 !_Gc ᵪ !.{R} Ṙ !k\=o ǭ !surd3 ∛ !austral ₳ !straightphi φ
!'s ś !Ga α !kU Ų !MCq 𝓺 !_Gf ᵩ !.{S} Ṡ !khei ϧ !surd4 ∜ !backsim ∽ !succcurlyeq ≽
!'u ú !Gb β !ka ą !MCr 𝓻 !_Gg ᵧ !.{T} Ṫ !k{A} Ą !tenge ₸ !because ∵ !succnapprox ⋩
!'w ẃ !Gc χ !ke ę !MCs 𝓼 !_Gr ᵨ !.{W} Ẇ !k{E} Ę !theta θ !between ≬ !thickapprox ≈
!'y ý !Gd δ !ki į !MCt 𝓽 !_lr ͍ !.{X} Ẋ !k{I} Į !times × !bigcirc ◯ !uncertainty ⯑
!'z ź !Ge ε !ko ǫ !MCu 𝓾 !all ∀ !.{Y} Ẏ !k{O} Ǫ !uplus ⊎ !bigodot ⨀ !updownarrow ↕
!(= !Gf φ !ku ų !MCv 𝓿 !and !.{Z} Ż !k{U} Ų !u{\i} ĭ !bigstar !^\Reversed E
!(b !Gg γ !l- !MCw 𝔀 !ast !.{a} ȧ !k{a} ą !vDash !bitcoin !^\Reversed N
!(| !Gh η !l= !MCx 𝔁 !bGG !.{b} !k{e} ę !varpi ϖ !boxplus !^\capital aa 𐞀
!)b !Gi ι !le !MCy 𝔂 !bGP !.{c} ċ !k{i} į !vdash !caution !^\capital oe 𐞣
!*= !Gk κ !ll !MCz 𝔃 !bGS !.{d} !k{o} ǫ !vdots !celsius !^\dz digraph 𐞇
!+ !Gl λ !lq !MIA 𝑨 !bGg !.{e} ė !k{u} ų !v{\i} ǐ !coloneq !^\ls digraph 𐞙
!-: !Gm μ !m= !MIB 𝑩 !bGp !.{f} !l-r- !v{\j} ǰ !ddagger !^\lz digraph 𐞚
!-> !Gn ν !mp !MIC 𝑪 !bot !.{g} ġ !lari !wedge !diamond !^\reversed e 𐞎
!-o !Go ω !mu μ !MID 𝑫 !bra !.{h} !lbag !~{\i} ĩ !digamma ϝ !^\sideways u
!-| !Gp ψ !ne !MIE 𝑬 !bub !.{m} !ldiv !"\'{I} Ḯ !dotplus ∔ !^\top half o ᵔ
!-~ !Gr ρ !ni !MIF 𝑭 !but !.{n} !leqq !"\'{U} Ǘ !drachma ₯ !^\ts digraph 𐞬
!.+ !Gs σ !nu ν !MIG 𝑮 !buw !.{o} ȯ !lira !"\'{i} ḯ !epsilon ϵ !blacklozenge ✦
!.- !Gt τ !o* !MIH 𝑯 !cap !.{p} !lneq !"\'{u} ǘ !eqarray █ !construction 🚧
!.= !Gu υ !o+ !MII 𝑰 !chi χ !.{r} !lnot ¬ !"\={A} Ǟ !eqcolon ≕ !ordmasculine º
!.A Ȧ !Gx ξ !o- !MIJ 𝑱 !ci. !.{s} !lr-- !"\={O} Ȫ !gtrless ≷ !risingdotseq ≓
!.B !Gz ζ !o. !MIK 𝑲 !ciO !.{t} !lr-n !"\={U} Ǖ !guarani ₲ !textcircledP ℗
!.C Ċ !HO Ő !o/ !MIL 𝑳 !cib !.{w} !lr=n !"\={a} ǟ !hryvnia ₴ !textdiscount ⁒
!.D !HU Ű !o= !MIM 𝑴 !ciw !.{x} !male !"\={o} ȫ !leadsto ↝ !triangledown ▿
!.E Ė !Ho ő !oe œ !MIN 𝑵 !clL !.{y} !mill !"\={u} ǖ !lessdot ⋖ !triangleleft ◃
!.F !Hu ű !oo !MIO 𝑶 !clR !.{z} ż !ngeq !"\`{U} Ǜ !lessgtr ≶ !Longleftarrow ⇐
!.G Ġ !Im !or !MIP 𝑷 !cll !<--> !ngtr !"\`{u} ǜ !lesssim ≲ !^\b with hook 𐞅
!.H !Ll !ox !MIQ 𝑸 !clr !<->n !nleq !"\v{U} Ǚ !lozenge ✧ !^\c with curl ᶝ
!.I İ !Mu Μ !pi π !MIR 𝑹 !cuL !<=>n !nmid !"\v{u} ǚ !maltese ✠ !^\d with hook 𐞌
!.M !Nu Ν !pm ± !MIS 𝑺 !cuR !<~nn !nsim !'\.{S} Ṥ !napprox ≉ !^\d with tail 𐞋
!.N !O* !r- !MIT 𝑻 !cul !=\"U Ṻ !odot ⊙ !'\.{s} ṥ !natural ♮ !^\g with hook 𐞓
!.O Ȯ !O+ !r= !MIU 𝑼 !cup !=\"u ṻ !oint ∮ !'{\AE} Ǽ !nearrow ↗ !^\greek gamma ᵞ
!.P !O. !rq !MIV 𝑽 !cur !=\'E Ḗ !perp ⊥ !'{\ae} ǽ !newline !^\h with hook ʱ
!.R !OE Œ !ss ß !MIW 𝑾 !c{} ¸ !=\'O Ṓ !peso ₱ !.\={A} Ǡ !nexists ∄ !^\l with belt 𐞛
!.S !Or !t= !MIX 𝑿 !d-2 !=\'e ḗ !prec ≺ !.\={O} Ȱ !nomisma 𐆎 !^\ligature oe ꟹ
!.T !Ox !th þ !MIY 𝒀 !d-| !=\'o ṓ !prod ∏ !.\={a} ǡ !npreceq ⋠ !^\m with hook ᶬ
!.W !Pi Π !to !MIZ 𝒁 !d== !=\AE Ǣ !qdrt !.\={o} ȱ !nsubset !^\r with tail 𐞨
!.X !Re !u+ !MIa 𝒂 !dag !=\`E !quad !=\"{U} Ṻ !nsucceq ⋡ !^\s with curl 𐞺
!.Y !TH Þ !u- !MIb 𝒃 !dd- !=\`O !r-l- !=\"{u} ṻ !nsupset ⊅ !^\s with hook ᶳ
!.Z Ż !U+ !u. !MIc 𝒄 !dei ϯ !=\`e !rbag !=\'{E} Ḗ !nwarrow ↖ !^\v with hook ᶹ
!.a ȧ !U. !u= !MId 𝒅 !di. !=\`o !rect !=\'{O} Ṓ !omicron ο !^\z with curl ᶽ
!.b !Un !uA Ă !MIe 𝒆 !dib !=\ae ǣ !rial !=\'{e} ḗ !partial ∂ !bigtriangleup △
!.c ċ !Uo ő !uE Ĕ !MIf 𝒇 !div ÷ !={A} Ā !sdiv !=\'{o} ṓ !phantom ⟡ !blacktriangle ▴
!.d !Xi Ξ !uG Ğ !MIg 𝒈 !diw !={E} Ē !shei ϣ !=\`{E} !pilcrow !divideontimes
!.e ė ![[ !uI Ĭ !MIh 𝒉 !dl- !={G} !sqrt !=\`{O} !ppprime !fallingdotseq
!.f !]] !uO Ŏ !MIi 𝒊 !dl= !={I} Ī !squb !=\`{e} !precsim !hookleftarrow
!.g ġ !^( !uU Ŭ !MIj 𝒋 !dr- !={O} Ō !squp !=\`{o} !searrow !leftarrowtail
!.h !^) !ua ă !MIk 𝒌 !dr= !={U} Ū !st12 !={\AE} Ǣ !section § !leftharpoonup
!.m !^+ !ue ĕ !MIl 𝒍 !ell !={Y} Ȳ !star !={\ae} ǣ !sqrt[3] !longleftarrow
!.n !^- !ug ğ !MIm 𝒎 !end !={a} ā !sub= !Bbb{1} 𝟙 !sqrt[4] !looparrowleft
!.o ȯ !^0 !ui ĭ !MIn 𝒏 !eta η !={e} ē !subn !Bbb{2} 𝟚 !succsim !measuredangle
!.p !^1 ¹ !un !MIo 𝒐 !exn !={g} !succ !Bbb{A} 𝔸 !swarrow !ntriangleleft
!.r !^2 ² !uo ŏ !MIp 𝒑 !fei ϥ !={i} ī !sup= !Bbb{B} 𝔹 !textwon !shortparallel
!.s !^3 ³ !uu ŭ !MIq 𝒒 !flq !={o} ō !supn !Bbb{C} !uparrow !smallsetminus
!.t !^4 !vA Ǎ !MIr 𝒓 !frq !={u} ū !surd !Bbb{D} 𝔻 !upsilon υ !textbigcircle
!.w !^5 !vC Č !MIs 𝒔 !gen !={y} ȳ !u-d- !Bbb{E} 𝔼 !varbeta ϐ !textestimated
!.x !^6 !vD Ď !MIt 𝒕 !ggg !>~nn !u\'A Ắ !Bbb{F} 𝔽 !warning ⚠ !triangleright ▹
!.y !^7 !vE Ě !MIu 𝒖 !glb !BGTH 𝚯 !u\'a ắ !Bbb{G} 𝔾 !BOmicron 𝚶 !upleftharpoon ↿
!.z ż !^8 !vG Ǧ !MIv 𝒗 !glq !BGth 𝛉 !u\`A !Bbb{H} !Bomicron 𝛐 !Leftrightarrow
!:: !^9 !vH Ȟ !MIw 𝒘 !grq !Beta Β !u\`a !Bbb{I} 𝕀 !^\h hook ʱ !Longrightarrow
!:= !^= !vI Ǐ !MIx 𝒙 !iff !Heta Ͱ !u\~A !Bbb{J} 𝕁 !^\open e !^\closed omega 𐞤
!:~ !^B !vK Ǩ !MIy 𝒚 !inf !Hori Ϩ !u\~a !Bbb{K} 𝕂 !^\open o !^\dezh digraph 𐞊
!<- !^D !vL Ľ !MIz 𝒛 !inn !H{O} Ő !ud-| !Bbb{L} 𝕃 !angstrom !^\feng digraph 𐞐
!<< !^F !vN Ň !McA 𝒜 !int !H{U} Ű !u{A} Ă !Bbb{M} 𝕄 !approxeq !^\tesh digraph 𐞮
!<n !^K !vO Ǒ !McB !kip !H{o} ő !u{E} Ĕ !Bbb{N} !backcong !^\turned alpha
!<| !^L !vR Ř !McC 𝒞 !k{} ˛ !H{u} ű !u{G} Ğ !Bbb{O} 𝕆 !barwedge !curvearrowleft
!<~ !^M !vS Š !McD 𝒟 !l-- !Iota Ι !u{I} Ĭ !Bbb{P} !bigoplus !downdownarrows
!=: !^N !vT Ť !McE !l-2 !Join !u{O} Ŏ !Bbb{Q} !bigsqcup !hookrightarrow
!== !^P !vU Ǔ !McF !l-> !Khei Ϧ !u{U} Ŭ !Bbb{R} !biguplus !leftleftarrows
!=> !^Q !vZ Ž !McG 𝒢 !l-n !Shei Ϣ !u{a} ă !Bbb{S} 𝕊 !bigwedge !leftrightarrow
!=A Ā !^R ᴿ !va ǎ !McH !l-| !U{o} ő !u{e} ĕ !Bbb{T} 𝕋 !boxminus !leftthreetimes
!=E Ē !^S Ŝ !vc č !McI !l== !Vert !u{g} ğ !Bbb{U} 𝕌 !boxtimes !longrightarrow
!=G !^T !vd ď !McJ 𝒥 !l=n !Zeta Ζ !u{i} ĭ !Bbb{V} 𝕍 !circledR ® !looparrowright
!=I Ī !^V !ve ě !McK 𝒦 !ldq !^Gth ᶿ !u{o} ŏ !Bbb{W} 𝕎 !circledS !multiplication ×
!=O Ō !^Y Ŷ !vg ǧ !McL !len !^\'A Ấ !u{u} ŭ !Bbb{X} 𝕏 !clubsuit ♣ !nshortparallel ∦
!=U Ū !^Z !vh ȟ !McM !lhd !^\'E Ế !v\.S Ṧ !Bbb{Y} 𝕐 !cruzeiro ₢ !ntriangleright ⋫
!=Y Ȳ !^b !vi ǐ !McN 𝒩 !ll- !^\'O Ố !v\.s ṧ !Bbb{Z} !curlyvee ⋎ !rightarrowtail ↣
!=a ā !^d !vj ǰ !McO 𝒪 !lr- !^\'a ấ !vbar │ !Bumpeq ≎ !currency ¤ !rightharpoonup ⇀
!=e ē !^f !vk ǩ !McP 𝒫 !lr= !^\'e ế !v{A} Ǎ !Frowny ☹ !diameter ⌀ !sphericalangle ∢
!=g !^k !vl ľ !McQ 𝒬 !lr~ !^\'o ố !v{C} Č !Gangia Ϫ !division ÷ !textopenbullet ◦
!=i ī !^m !vn ň !McR !lub !^\Ae !v{D} Ď !Lambda Λ !doteqdot !trianglelefteq
!=n !^n !vo ǒ !McS 𝒮 !mho !^\Ou !v{E} Ě !Letter !emptyset !uprightharpoon
!=u ū !^p !vr ř !McT 𝒯 !mid !^\`A !v{G} Ǧ !Smiley !geqslant !^\H With Stroke
!=y ȳ !^q 𐞥 !vs š !McU 𝒰 !neg ¬ !^\`E !v{H} Ȟ !Stigma Ϛ !gnapprox !^\bottom half o
!>= !^t !vt ť !McV 𝒱 !neq !^\`O !v{I} Ǐ !Subset !hphantom !^\h with stroke 𐞕
!>> !^x ˣ !vu ǔ !McW 𝒲 !nin !^\`a !v{K} Ǩ !Supset !intercal !^\i with stroke
!>n !_( !vz ž !McX 𝒳 !not ̸ !^\`e !v{L} Ľ !Vvdash !leqslant !^\o with stroke 𐞢
!>~ !_) !wp !McY 𝒴 !o-- !^\`o !v{N} Ň !^\'{A} Ấ !llcorner ⌞ !^\turned open e ᵌ
!?= !_+ !wr !McZ 𝒵 !ohm !^\ae 𐞃 !v{O} Ǒ !^\'{E} Ế !lnapprox ⋦ !^\turned r hook ʵ
!?? !_- !xi ξ !Mca 𝒶 !or= !^\~A !v{R} Ř !^\'{O} Ố !lrcorner ⌟ !bigtriangledown ▽
!AA Å !_0 !z: !Mcb 𝒷 !pab !^\~E !v{S} Š !^\'{a} ấ !multimap ⊸ !circlearrowleft ↺
!AE Æ !_1 !{{ !Mcc 𝒸 !paw !^\~O !v{T} Ť !^\'{e} ế !parallel ∥ !curvearrowright ↷
!B0 𝟎 !_2 !|) !Mcd 𝒹 !per !^\~a !v{U} Ǔ !^\'{o} ố !pppprime ⁗ !downleftharpoon ⇃
!B1 𝟏 !_3 !|- !Mce !phi ϕ !^\~e !v{Z} Ž !^\`{A} !precnsim !leftharpoondown
!B2 𝟐 !_4 !|= !Mcf 𝒻 !psi ψ !^\~o !v{a} ǎ !^\`{E} !setminus !leftrightarrows
!B3 𝟑 !_5 !|> !Mcg !qed !^{A} Â !v{c} č !^\`{O} !shortmid !nLeftrightarrow
!B4 𝟒 !_6 !|n !Mch 𝒽 !r-- !^{C} Ĉ !v{d} ď !^\`{a} !spesmilo !nleftrightarrow
!B5 𝟓 !_7 !|| !Mci 𝒾 !r-2 !^{E} Ê !v{e} ě !^\`{e} !sqsubset !ntrianglelefteq
!B6 𝟔 !_8 !}} !Mcj 𝒿 !r-3 !^{G} Ĝ !v{g} ǧ !^\`{o} !sqsupset !rightleftarrows
!B7 𝟕 !_9 !~- !Mck 𝓀 !r-> !^{H} Ĥ !v{h} ȟ !^\beta !subseteq !rightthreetimes
!B8 𝟖 !_= !~= !Mcl 𝓁 !r-n !^{I} Î !v{i} ǐ !^\d{A} !succnsim !squigarrowright
!B9 𝟗 !__ _ !~A Ã !Mcm 𝓂 !r-o !^{J} Ĵ !v{j} ǰ !^\d{E} !supseteq !textinterrobang
!BA 𝐀 !_a !~E !Mcn 𝓃 !r-| !^{O} Ô !v{k} ǩ !^\d{O} !textbaht ฿ !textmusicalnote
!BB 𝐁 !_e !~I Ĩ !Mco !r== !^{S} Ŝ !v{l} ľ !^\d{a} !textdied !trianglerighteq
!BC 𝐂 !_h !~N Ñ !Mcp 𝓅 !r=n !^{U} Û !v{n} ň !^\d{e} !textlira !vartriangleleft
!BD 𝐃 !_i !~O Õ !Mcq 𝓆 !rdq !^{W} Ŵ !v{o} ǒ !^\d{o} !textpeso !^\heng with hook 𐞗
!BE 𝐄 !_j !~U Ũ !Mcr 𝓇 !rhd !^{Y} Ŷ !v{r} ř !^\heng !thicksim !circlearrowright
!BF 𝐅 !_k !~V !Mcs 𝓈 !rho ρ !^{Z} !v{s} š !^\iota !triangle !downrightharpoon
!BG 𝐆 !_l !~Y !Mct 𝓉 !rr- !^{a} â !v{t} ť !^\lezh 𐞞 !ulcorner !ntrianglerighteq
!BH 𝐇 !_m !~a ã !Mcu 𝓊 !san ϻ !^{c} ĉ !v{u} ǔ !^\~{A} !underbar !rightharpoondown
!BI 𝐈 !_n !~e !Mcv 𝓋 !sbs !^{e} ê !v{z} ž !^\~{E} !undertie !rightrightarrows
!BJ 𝐉 !_o !~i ĩ !Mcw 𝓌 !sho ϸ !^{g} ĝ !zeta ζ !^\~{O} !urcorner !twoheadleftarrow
!BK 𝐊 !_p !~o õ !Mcx 𝓍 !sim !^{h} ĥ !||-n !^\~{a} !varkappa ϰ !vartriangleright
!BL 𝐋 !_r !~u ũ !Mcy 𝓎 !som !^{i} î !||=n !^\~{e} !varprime !^\r with fishhook 𐞩
!BM 𝐌 !_s !~v !Mcz 𝓏 !sq. !^{j} ĵ !|||- !^\~{o} !varsigma ς !^\reversed open e
!BN 𝐍 !_t !~y !MfA 𝔄 !sqo !^{o} ô !~\"O Ṏ !^{TEL} ℡ !vartheta ϑ !blacktriangledown ▾
!BO 𝐎 !_u !~~ !MfB 𝔅 !st6 !^{s} ŝ !~\"o ṏ !approx ≈ !vphantom ⇳ !blacktriangleleft ◂
!BP 𝐏 !_x !"{} ¨ !MfC !st8 ✴ !^{u} û !~\'O Ṍ !asmash ⬆ !Downarrow ⇓ !leftrightharpoons ⇋
!BQ 𝐐 !_~ ̰ !'\O Ǿ !MfD 𝔇 !sub ⊂ !^{w} ŵ !~\'U Ṹ !bigcap ⋂ !Leftarrow ⇐ !rightleftharpoons ⇌
!BR 𝐑 !`A À !'\o ǿ !MfE 𝔈 !sum ∑ !^{y} ŷ !~\'o ṍ !bigcup !^\upsilon ᶷ !textcolonmonetary ₡
!BS 𝐒 !`E È !'{} ´ !MfF 𝔉 !sup ⊃ !^{z} ẑ !~\'u ṹ !bigvee !backprime !textreferencemark ※
!BT 𝐓 !`I Ì !--> !MfG 𝔊 !tau τ !`{A} À !~\=O Ȭ !bowtie !backsimeq !twoheadrightarrow
!BU 𝐔 !`N Ǹ !->n !MfH !tie !`{E} È !~\=o ȭ !bumpeq !bigotimes !Longleftrightarrow
!BV 𝐕 !`O Ò !.=. !MfI !top !`{I} Ì !~{A} Ã !c\'{C} Ḉ !biohazard ☣ !^\n with left hook ᶮ
!BW 𝐖 !`U Ù !.{} ˙ !MfJ 𝔍 !u-2 !`{N} Ǹ !~{E} !c\'{c} ḉ !brokenbar ¦ !^\u with left hook ꭟ
!BX 𝐗 !`W !::- !MfK 𝔎 !u-| !`{O} Ò !~{I} Ĩ !c\u{E} !centerdot · !blacktriangleright
!BY 𝐘 !`Y !<-- !MfL 𝔏 !u== !`{U} Ù !~{N} Ñ !c\u{e} !checkmark !longleftrightarrow
!BZ 𝐙 !`a à !<-> !MfM 𝔐 !ud- !`{W} !~{O} Õ !circeq !copyright © !textpertenthousand
!Ba 𝐚 !`e è !<-n !MfN 𝔑 !ud= !`{Y} !~{U} Ũ !coprod !dotsquare !^\v with right hook 𐞰
!Bb 𝐛 !`i ì !<=> !MfO 𝔒 !ul- !`{a} à !~{V} !d\.{S} !downarrow !leftrightsquigarrow
!Bc 𝐜 !`n ǹ !<=n !MfP 𝔓 !ul= !`{e} è !~{Y} !d\.{s} !facsimile !textfractionsolidus
!Bd 𝐝 !`o ò !<~n !MfQ 𝔔 !ur- !`{i} ì !~{a} ã !d\={L} !gtrapprox !^\capital inverted r ʶ
!Be 𝐞 !`u ù !=== !MfR !ur= !`{n} ǹ !~{e} !d\={R} !gtreqless !^\turned r with hook ʵ
!Bf 𝐟 !`w !==n !MfS 𝔖 !uu- !`{o} ò !~{i} ĩ !d\={l} !gvertneqq !^\turned y with belt 𐞡
!Bg 𝐠 !`y !=>n !MfT 𝔗 !u{} ˘ !`{u} ù !~{n} ñ !d\={r} !heartsuit !^\capital g with hook 𐞔
!Bh 𝐡 !aa å !={} ¯ !MfU 𝔘 !vee !`{w} !~{o} õ !dagger !increment !^\capital l with belt 𐞜
!Bi 𝐢 !ae æ !>=n !MfV 𝔙 !v{} ˇ !`{y} !~{u} ũ !daleth !lambdabar ƛ !^\j with crossed-tail
!Bj 𝐣 !b+ !>~n !MfW 𝔚 !won !and= !~{v} !ddddot !leftarrow !^\l with middle tilde
!Bk 𝐤 !b- !And !MfX 𝔛 !yen ¥ !atop ¦ !~{y} !degree ° !lesseqgtr !^\l with palatal hook
!Bl 𝐥 !b. !BGA 𝚨 !MfY 𝔜 !|-n !beta β !'{\O} Ǿ !dsmash ⬇ !llbracket 〚 !^\t with palatal hook ᶵ
!Bm 𝐦 !b0 𝟘 !BGB 𝚩 !MfZ !|=n !beth !'{\o} ǿ !eqcirc ≖ !lvertneqq ≨ !^\d with hook and tail 𐞍
!Bn 𝐧 !b1 𝟙 !BGC 𝚾 !Mfa 𝔞 !||- !c\'C Ḉ !={\i} ī !exists ∃ !ngeqslant ≱ !^\dz digraph with curl 𐞉
!Bo 𝐨 !b2 𝟚 !BGD 𝚫 !Mfb 𝔟 !||= !c\'c ḉ !Alpha Α !female ♀ !nleqslant ≰ !^\tc digraph with curl 𐞫
!Bp 𝐩 !b3 𝟛 !BGE 𝚬 !Mfc 𝔠 !||n !c\uE !Delta Δ !forall !nparallel !^\capital i with stroke
!Bq 𝐪 !b4 𝟜 !BGF 𝚽 !Mfd 𝔡 !~-n !c\ue !Gamma Γ !frac12 ½ !nshortmid !^\dotless j with stroke
!Br 𝐫 !b5 𝟝 !BGG 𝚪 !Mfe 𝔢 !~=n !cdot · !Kappa Κ !frac13 !nsubseteq !^\l with retroflex hook
!Bs 𝐬 !b6 𝟞 !BGH 𝚮 !Mff 𝔣 !~{} ˜ !cedi !Koppa Ϟ !frac14 ¼ !nsupseteq !^\n with retroflex hook
!Bt 𝐭 !b7 𝟟 !BGI 𝚰 !Mfg 𝔤 !~~- !cent ¢ !Lamda Λ !frac15 !octagonal 🛑 !^\reversed glottal stop ˤ
!Bu 𝐮 !b8 𝟠 !BGK 𝚱 !Mfh 𝔥 !~~n !ci.. !Omega Ω !frac16 !overbrace !^\t with retroflex hook 𐞯
!Bv 𝐯 !b9 𝟡 !BGL 𝚲 !Mfi 𝔦 !~~~ !circ !Sampi Ϡ !frac18 !overparen !^\z with retroflex hook
!Bw 𝐰 !bA 𝔸 !BGM 𝚳 !Mfj 𝔧 !"\'I Ḯ !comp ∘ !Shima Ϭ !frac23 ⅔ !paragraph ¶ !^\closed reversed open e 𐞏
!Bx 𝐱 !bB 𝔹 !BGN 𝚴 !Mfk 𝔨 !"\'U Ǘ !cong ≅ !Sigma Σ !frac25 ⅖ !pitchfork ⋔ !^\l with inverted lazy s ꭝ
!By 𝐲 !bC !BGO 𝛀 !Mfl 𝔩 !"\'i ḯ !c{C} Ç !Theta Θ !frac34 ¾ !rrbracket 〛 !^\turned m with long leg ᶭ
!Bz 𝐳 !bD 𝔻 !BGP 𝚿 !Mfm 𝔪 !"\'u ǘ !c{D} Ḑ !Vdash ⊩ !frac35 ⅗ !spadesuit ♠ !^\turned r with long leg 𐞦
!DH Ð !bE 𝔼 !BGR 𝚸 !Mfn 𝔫 !"\=A Ǟ !c{E} Ȩ !^\ain ᵜ !frac38 ⅜ !subseteqq ⊆ !^\lezh with retroflex hook 𐞟
!Dd !bF 𝔽 !BGS 𝚺 !Mfo 𝔬 !"\=O Ȫ !c{G} Ģ !^\chi ᵡ !frac45 ⅘ !subsetneq ⊊ !^\dotless j with stroke and hook 𐞘
!F0 !bG 𝔾 !BGT 𝚻 !Mfp 𝔭 !"\=U Ǖ !c{H} Ḩ !^\eng ᵑ !frac56 ⅚ !supseteqq ⊇ !^\dz digraph with retroflex hook 𐞈
!F1 !bH !BGU 𝚼 !Mfq 𝔮 !"\=a ǟ !c{K} Ķ !^\esh ᶴ !frac58 ⅝ !supsetneq ⊋ !^\l with retroflex hook and belt 𐞝
!F2 !bI 𝕀 !BGX 𝚵 !Mfr 𝔯 !"\=o ȫ !c{L} Ļ !^\eth ᶞ !frac78 ⅞ !telephone ℡ !^\ts digraph with retroflex hook 𐞭
!F3 !bJ 𝕁 !BGZ 𝚭 !Mfs 𝔰 !"\=u ǖ !c{N} Ņ !^\ezh ᶾ !gangia ϫ !textnaira ₦ !^\turned r with long leg and retroflex hook 𐞧
!F4 !bK 𝕂 !BGa 𝛂 !Mft 𝔱 !"\`U Ǜ !c{R} Ŗ !^\phi ᶲ !gtrdot ⋗ !therefore ∴
!F5 !bL 𝕃 !BGb 𝛃 !Mfu 𝔲 !"\`u ǜ !c{S} Ş !^{SM} ℠ !gtrsim ≳ !triangleq ≜
!F6 !bM 𝕄 !BGc 𝛘 !Mfv 𝔳 !"\vU Ǚ !c{T} Ţ !^{TM} ™ !hsmash ⬌ !varpropto ∝
!F7 !bN !BGd 𝛅 !Mfw 𝔴 !"\vu ǚ !c{c} ç !^{\j} ĵ !iiiint ⨌ !Lleftarrow ⇚
!F8 !bO 𝕆 !BGe 𝛆 !Mfx 𝔵 !"{A} Ä !c{d} ḑ !above ┴ !k\={O} Ǭ !Rightarrow ⇒
!F9 !bP !BGf 𝛗 !Mfy 𝔶 !"{E} Ë !c{e} ȩ !aleph ℵ !k\={o} ǭ !^\Barred B ᴯ
!FA !bQ !BGg 𝛄 !Mfz 𝔷 !"{H} Ḧ !c{g} ģ !alpha α !kelvin !^\barred o ᶱ
"""
agda_words = extras + parse_source(source)
if __name__ == "__main__":
print(f"{len(agda_words)} keybinds")