Fcitx 5 Quick Phrase for Agda Input

agda.mb

\eq =
\eq ∼
\eq ∽
\eq ≈
\eq ≋
\eq ∻
\eq ∾
\eq ∿
\eq ≀
\eq ≃
\eq ⋍
\eq ≂
\eq ≅
\eq ≌
\eq ≊
\eq ≡
\eq ≣
\eq ≐
\eq ≑
\eq ≒
\eq ≓
\eq ≔
\eq ≕
\eq ≖
\eq ≗
\eq ≘
\eq ≙
\eq ≚
\eq ≛
\eq ≜
\eq ≝
\eq ≞
\eq ≟
\eq ≍
\eq ≎
\eq ≏
\eq ≬
\eq ⋕
\eqn ≠
\eqn ≁
\eqn ≉
\eqn ≄
\eqn ≇
\eqn ≆
\eqn ≢
\eqn ≭
\=n ≠
\~ ∼
\~n ≁
\~~ ≈
\~~n ≉
\~~~ ≋
\:~ ∻
\~- ≃
\~-n ≄
\-~ ≂
\~= ≅
\~=n ≇
\~~- ≊
\== ≡
\==n ≢
\=== ≣
\.= ≐
\.=. ≑
\:= ≔
\=: ≕
\=o ≗
\(= ≘
\and= ≙
\or= ≚
\*= ≛
\t= ≜
\def= ≝
\m= ≞
\?= ≟
\leq <
\leq ≪
\leq ⋘
\leq ≤
\leq ≦
\leq ≲
\leq ≶
\leq ≺
\leq ≼
\leq ≾
\leq ⊂
\leq ⊆
\leq ⋐
\leq ⊏
\leq ⊑
\leq ⊰
\leq ⊲
\leq ⊴
\leq ⋖
\leq ⋚
\leq ⋜
\leq ⋞
\leqn ≮
\leqn ≰
\leqn ≨
\leqn ≴
\leqn ⋦
\leqn ≸
\leqn ⊀
\leqn ⋨
\leqn ⊄
\leqn ⊈
\leqn ⊊
\leqn ⋢
\leqn ⋤
\leqn ⋪
\leqn ⋬
\leqn ⋠
\geq >
\geq ≫
\geq ⋙
\geq ≥
\geq ≧
\geq ≳
\geq ≷
\geq ≻
\geq ≽
\geq ≿
\geq ⊃
\geq ⊇
\geq ⋑
\geq ⊐
\geq ⊒
\geq ⊱
\geq ⊳
\geq ⊵
\geq ⋗
\geq ⋛
\geq ⋝
\geq ⋟
\geqn ≯
\geqn ≱
\geqn ≩
\geqn ≵
\geqn ⋧
\geqn ≹
\geqn ⊁
\geqn ⋩
\geqn ⊅
\geqn ⊉
\geqn ⊋
\geqn ⋣
\geqn ⋥
\geqn ⋫
\geqn ⋭
\geqn ⋡
\<= ≤
\>= ≥
\<=n ≰
\>=n ≱
\len ≰
\gen ≱
\<n ≮
\>n ≯
\<~ ≲
\>~ ≳
\<~n ⋦
\>~n ⋧
\<~nn ≴
\>~nn ≵
\sub ⊂
\sup ⊃
\subn ⊄
\supn ⊅
\sub= ⊆
\sup= ⊇
\sub=n ⊈
\sup=n ⊉
\squb ⊏
\squp ⊐
\squb= ⊑
\squp= ⊒
\squb=n ⋢
\squp=n ⋣
\member ∈
\member ∉
\member ∊
\member ∋
\member ∌
\member ∍
\member ⋲
\member ⋳
\member ⋴
\member ⋵
\member ⋶
\member ⋷
\member ⋸
\member ⋹
\member ⋺
\member ⋻
\member ⋼
\member ⋽
\member ⋾
\member ⋿
\inn ∉
\nin ∌
\intersection ∩
\intersection ⋂
\intersection ∧
\intersection ⋀
\intersection ⋏
\intersection ⨇
\intersection ⊓
\intersection ⨅
\intersection ⋒
\intersection ∏
\intersection ⊼
\intersection ⨉
\union ∪
\union ⋃
\union ∨
\union ⋁
\union ⋎
\union ⨈
\union ⊔
\union ⨆
\union ⋓
\union ∐
\union ⨿
\union ⊽
\union ⊻
\union ⊍
\union ⨃
\union ⊎
\union ⨄
\union ⊌
\union ∑
\union ⅀
\and ∧
\or ∨
\And ⋀
\Or ⋁
\i ∩
\un ∪
\u+ ⊎
\u. ⊍
\I ⋂
\Un ⋃
\U+ ⨄
\U. ⨃
\glb ⊓
\lub ⊔
\Glb ⨅
\Lub ⨆
\entails ⊢
\entails ⊣
\entails ⊤
\entails ⊥
\entails ⊦
\entails ⊧
\entails ⊨
\entails ⊩
\entails ⊪
\entails ⊫
\entails ⊬
\entails ⊭
\entails ⊮
\entails ⊯
\|- ⊢
\|-n ⊬
\-| ⊣
\|= ⊨
\|=n ⊭
\||- ⊩
\||-n ⊮
\||= ⊫
\||=n ⊯
\|||- ⊪
\| ∣
\|n ∤
\|| ∥
\||n ∦
\all ∀
\ex ∃
\exn ∄
\0 ∅
\C ∁
\c ⌜
\c ⌝
\c ⌞
\c ⌟
\c ⌈
\c ⌉
\c ⌊
\c ⌋
\cu ⌜
\cu ⌝
\cu ⌈
\cu ⌉
\cl ⌞
\cl ⌟
\cl ⌊
\cl ⌋
\cul ⌜
\cuL ⌈
\cur ⌝
\cuR ⌉
\cll ⌞
\clL ⌊
\clr ⌟
\clR ⌋
\qed ∎
\x ×
\o ∘
\comp ∘
\. ∙
\* ⋆
\.+ ∔
\.- ∸
\: ∶
\: ⦂
\: ː
\: ꞉
\: ˸
\: ፥
\: ፦
\: ：
\: ﹕
\: ︓
\, ʻ
\, ،
\, ⸲
\, ⸴
\, ⹁
\, ⹉
\, 、
\, ︐
\, ︑
\, ﹐
\, ﹑
\, ，
\, ､
\; ؛
\; ⁏
\; ፤
\; ꛶
\; ；
\; ︔
\; ﹔
\; ⍮
\; ⸵
\; ;
\:: ∷
\::- ∺
\-: ∹
\+  ⊹
\surd3 ∛
\surd4 ∜
\increment ∆
\inf ∞
\& ⅋
\z; ⨟
\z: ⦂
\o+ ⊕
\o-- ⊖
\ox ⊗
\o/ ⊘
\o. ⊙
\oo ⊚
\o* ⊛
\o= ⊜
\o- ⊝
\O+ ⨁
\Ox ⨂
\O. ⨀
\O* ⍟
\b+ ⊞
\b- ⊟
\bx ⊠
\b. ⊡
\integral ∫
\integral ∬
\integral ∭
\integral ∮
\integral ∯
\integral ∰
\integral ∱
\integral ∲
\integral ∳
\angle ∟
\angle ∡
\angle ∢
\angle ⊾
\angle ⊿
\join ⋈
\join ⋉
\join ⋊
\join ⋋
\join ⋌
\join ⨝
\join ⟕
\join ⟖
\join ⟗
\l ←
\l ⇐
\l ⇚
\l ⇇
\l ⇆
\l ↤
\l ⇦
\l ↞
\l ↼
\l ↽
\l ⇠
\l ⇺
\l ↜
\l ⇽
\l ⟵
\l ⟸
\l ↚
\l ⇍
\l ⇷
\l ↹
\l ↢
\l ↩
\l ↫
\l ⇋
\l ⇜
\l ⇤
\l ⟻
\l ⟽
\l ⤆
\l ↶
\l ↺
\l ⟲
\r →
\r ⇒
\r ⇛
\r ⇉
\r ⇄
\r ↦
\r ⇨
\r ↠
\r ⇀
\r ⇁
\r ⇢
\r ⇻
\r ↝
\r ⇾
\r ⟶
\r ⟹
\r ↛
\r ⇏
\r ⇸
\r ⇶
\r ↴
\r ↣
\r ↪
\r ↬
\r ⇌
\r ⇝
\r ⇥
\r ⟼
\r ⟾
\r ⤇
\r ↷
\r ↻
\r ⟳
\r ⇰
\r ⇴
\r ⟴
\r ⟿
\r ➵
\r ➸
\r ➙
\r ➔
\r ➛
\r ➜
\r ➝
\r ➞
\r ➟
\r ➠
\r ➡
\r ➢
\r ➣
\r ➤
\r ➧
\r ➨
\r ➩
\r ➪
\r ➫
\r ➬
\r ➭
\r ➮
\r ➯
\r ➱
\r ➲
\r ➳
\r ➺
\r ➻
\r ➼
\r ➽
\r ➾
\r ⊸
\u ↑
\u ⇑
\u ⟰
\u ⇈
\u ⇅
\u ↥
\u ⇧
\u ↟
\u ↿
\u ↾
\u ⇡
\u ⇞
\u ↰
\u ↱
\u ➦
\u ⇪
\u ⇫
\u ⇬
\u ⇭
\u ⇮
\u ⇯
\d ↓
\d ⇓
\d ⟱
\d ⇊
\d ⇵
\d ↧
\d ⇩
\d ↡
\d ⇃
\d ⇂
\d ⇣
\d ⇟
\d ↵
\d ↲
\d ↳
\d ➥
\d ↯
\ud ↕
\ud ⇕
\ud ↨
\ud ⇳
\lr ↔
\lr ⇔
\lr ⇼
\lr ↭
\lr ⇿
\lr ⟷
\lr ⟺
\lr ↮
\lr ⇎
\lr ⇹
\ul ↖
\ul ⇖
\ul ⇱
\ul ↸
\ur ↗
\ur ⇗
\ur ➶
\ur ➹
\ur ➚
\dr ↘
\dr ⇘
\dr ⇲
\dr ➴
\dr ➷
\dr ➘
\dl ↙
\dl ⇙
\l- ←
\<- ←
\l= ⇐
\<= ⇐
\r- →
\-> →
\r= ⇒
\=> ⇒
\u- ↑
\u= ⇑
\d- ↓
\d= ⇓
\ud- ↕
\ud= ⇕
\lr- ↔
\<-> ↔
\lr= ⇔
\<=> ⇔
\ul- ↖
\ul= ⇖
\ur- ↗
\ur= ⇗
\dr- ↘
\dr= ⇘
\dl- ↙
\dl= ⇙
\l== ⇚
\l-2 ⇇
\l-r- ⇆
\r== ⇛
\r-2 ⇉
\r-3 ⇶
\r-l- ⇄
\u== ⟰
\u-2 ⇈
\u-d- ⇅
\d== ⟱
\d-2 ⇊
\d-u- ⇵
\l-- ⟵
\<-- ⟵
\l~ ↜
\l~ ⇜
\r-- ⟶
\--> ⟶
\r~ ↝
\r~ ⇝
\r~ ⟿
\lr-- ⟷
\<--> ⟷
\lr~ ↭
\l-n ↚
\<-n ↚
\l=n ⇍
\r-n ↛
\->n ↛
\r=n ⇏
\=>n ⇏
\lr-n ↮
\<->n ↮
\lr=n ⇎
\<=>n ⇎
\l-| ↤
\ll- ↞
\r-| ↦
\rr- ↠
\u-| ↥
\uu- ↟
\d-| ↧
\dd- ↡
\ud-| ↨
\l-> ↢
\r-> ↣
\r-o ⊸
\-o ⊸
\dz ↯
\... ⋯
\... ⋮
\... ⋰
\... ⋱
\--- ─
\--- │
\--- ┌
\--- ┐
\--- └
\--- ┘
\--- ├
\--- ┤
\--- ┬
\--- ┼
\--- ┴
\--- ╴
\--- ╵
\--- ╶
\--- ╷
\--- ╭
\--- ╮
\--- ╯
\--- ╰
\--- ╱
\--- ╲
\--- ╳
\--= ═
\--= ║
\--= ╔
\--= ╗
\--= ╚
\--= ╝
\--= ╠
\--= ╣
\--= ╦
\--= ╬
\--= ╩
\--= ╒
\--= ╕
\--= ╘
\--= ╛
\--= ╞
\--= ╡
\--= ╤
\--= ╪
\--= ╧
\--= ╓
\--= ╖
\--= ╙
\--= ╜
\--= ╟
\--= ╢
\--= ╥
\--= ╫
\--= ╨
\--_ ━
\--_ ┃
\--_ ┏
\--_ ┓
\--_ ┗
\--_ ┛
\--_ ┣
\--_ ┫
\--_ ┳
\--_ ╋
\--_ ┻
\--_ ╸
\--_ ╹
\--_ ╺
\--_ ╻
\--_ 

\--_ ┍
\--_ ┯
\--_ ┑
\--_ ┕
\--_ ┷
\--_ ┙
\--_ ┝
\--_ ┿
\--_ ┥
\--_ ┎
\--_ ┰
\--_ ┒
\--_ ┖
\--_ ┸
\--_ ┚
\--_ ┠
\--_ ╂
\--_ ┨
\--_ ┞
\--_ ╀
\--_ ┦
\--_ ┟
\--_ ╁
\--_ ┧
\--_ ┢
\--_ ╈
\--_ ┪
\--_ ┡
\--_ ╇
\--_ ┩
\--_ 

\--_ ┮
\--_ ┭
\--_ ┶
\--_ ┵
\--_ ┾
\--_ ┽
\--_ ┲
\--_ ┱
\--_ ┺
\--_ ┹
\--_ ╊
\--_ ╉
\--_ ╆
\--_ ╅
\--_ ╄
\--_ ╃
\--_ ╿
\--_ ╽
\--_ ╼
\--_ ╾
\--. ╌
\--. ╎
\--. ┄
\--. ┆
\--. ┈
\--. ┊
\--. 

\--. ╍
\--. ╏
\--. ┅
\--. ┇
\--. ┉
\--. ┋
\t ◂
\t ◃
\t ◄
\t ◅
\t ▸
\t ▹
\t ►
\t ▻
\t ▴
\t ▵
\t ▾
\t ▿
\t ◢
\t ◿
\t ◣
\t ◺
\t ◤
\t ◸
\t ◥
\t ◹
\T ◀
\T ◁
\T ▶
\T ▷
\T ▲
\T △
\T ▼
\T ▽
\T ◬
\T ◭
\T ◮
\tb ◂
\tb ▸
\tb ▴
\tb ▾
\tb ◄
\tb ►
\tb ◢
\tb ◣
\tb ◤
\tb ◥
\tw ◃
\tw ▹
\tw ▵
\tw ▿
\tw ◅
\tw ▻
\tw ◿
\tw ◺
\tw ◸
\tw ◹
\Tb ◀
\Tb ▶
\Tb ▲
\Tb ▼
\Tw ◁
\Tw ▷
\Tw △
\Tw ▽
\sq ■
\sq □
\sq ◼
\sq ◻
\sq ◾
\sq ◽
\sq ▣
\sq ▢
\sq ▤
\sq ▥
\sq ▦
\sq ▧
\sq ▨
\sq ▩
\sq ◧
\sq ◨
\sq ◩
\sq ◪
\sq ◫
\sq ◰
\sq ◱
\sq ◲
\sq ◳
\sqb ■
\sqb ◼
\sqb ◾
\sqw □
\sqw ◻
\sqw ◽
\sq. ▣
\sqo ▢
\re ▬
\re ▭
\re ▮
\re ▯
\reb ▬
\reb ▮
\rew ▭
\rew ▯
\pa ▰
\pa ▱
\pab ▰
\paw ▱
\di ◆
\di ◇
\di ◈
\dib ◆
\diw ◇
\di. ◈
\ci ●
\ci ○
\ci ◎
\ci ◌
\ci ◯
\ci ◍
\ci ◐
\ci ◑
\ci ◒
\ci ◓
\ci ◔
\ci ◕
\ci ◖
\ci ◗
\ci ◠
\ci ◡
\ci ◴
\ci ◵
\ci ◶
\ci ◷
\ci ⚆
\ci ⚇
\ci ⚈
\ci ⚉
\cib ●
\ciw ○
\ci. ◎
\ci.. ◌
\ciO ◯
\st ⋆
\st ✦
\st ✧
\st ✶
\st ✴
\st ✹
\st ★
\st ☆
\st ✪
\st ✫
\st ✯
\st ✰
\st ✵
\st ✷
\st ✸
\st4 ✦
\st4 ✧
\st6 ✶
\st8 ✴
\st12 ✹
\bA 𝔸
\bB 𝔹
\bC ℂ
\bD 𝔻
\bE 𝔼
\bF 𝔽
\bG 𝔾
\bH ℍ
\bI 𝕀
\bJ 𝕁
\bK 𝕂
\bL 𝕃
\bM 𝕄
\bN ℕ
\bO 𝕆
\bP ℙ
\bQ ℚ
\bR ℝ
\bS 𝕊
\bT 𝕋
\bU 𝕌
\bV 𝕍
\bW 𝕎
\bX 𝕏
\bY 𝕐
\bZ ℤ
\bGG ℾ
\bGP ℿ
\bGS ⅀
\ba 𝕒
\bb 𝕓
\bc 𝕔
\bd 𝕕
\be 𝕖
\bf 𝕗
\bg 𝕘
\bh 𝕙
\bi 𝕚
\bj 𝕛
\bk 𝕜
\bl 𝕝
\bm 𝕞
\bn 𝕟
\bo 𝕠
\bp 𝕡
\bq 𝕢
\br 𝕣
\bs 𝕤
\bt 𝕥
\bu 𝕦
\bv 𝕧
\bw 𝕨
\bx 𝕩
\by 𝕪
\bz 𝕫
\bGg ℽ
\bGp ℼ
\b0 𝟘
\b1 𝟙
\b2 𝟚
\b3 𝟛
\b4 𝟜
\b5 𝟝
\b6 𝟞
\b7 𝟟
\b8 𝟠
\b9 𝟡
\B0 𝟎
\B1 𝟏
\B2 𝟐
\B3 𝟑
\B4 𝟒
\B5 𝟓
\B6 𝟔
\B7 𝟕
\B8 𝟖
\B9 𝟗
\( (
\( [
\( {
\( ⁅
\( ⁽
\( ₍
\( 〈
\( ⎴
\( ⟅
\( ⟦
\( ⟨
\( ⟪
\( ⦃
\( 〈
\( 《
\( 「
\( 『
\( 【
\( 〔
\( 〖
\( 〚
\( ︵
\( ︷
\( ︹
\( ︻
\( ︽
\( ︿
\( ﹁
\( ﹃
\( ﹙
\( ﹛
\( ﹝
\( （
\( ［
\( ｛
\( ｢
\( ❪
\( ❬
\( ❰
\( ❲
\( ❴
\( ⟮
\( ⦅
\( ⦗
\( ⧼
\( ⸨
\( ❮
\( ⦇
\( ⦉
\) )
\) ]
\) }
\) ⁆
\) ⁾
\) ₎
\) 〉
\) ⎵
\) ⟆
\) ⟧
\) ⟩
\) ⟫
\) ⦄
\) 〉
\) 》
\) 」
\) 』
\) 】
\) 〕
\) 〗
\) 〛
\) ︶
\) ︸
\) ︺
\) ︼
\) ︾
\) ﹀
\) ﹂
\) ﹄
\) ﹚
\) ﹜
\) ﹞
\) ）
\) ］
\) ｝
\) ｣
\) ❫
\) ❭
\) ❱
\) ❳
\) ❵
\) ⟯
\) ⦆
\) ⦘
\) ⧽
\) ⸩
\) ❯
\) ⦈
\) ⦊
\[[ ⟦
\]] ⟧
\< ⟨
\> ⟩
\<< ⟪
\>> ⟫
\{{ ⦃
\}} ⦄
\(b ⟅
\)b ⟆
\lbag ⟅
\rbag ⟆
\<| ⦉
\|> ⦊
\(| ⦇
\|) ⦈
\(( ⦅
\)) ⦆
\' ′
\' ″
\' ‴
\' ⁗
\` ‵
\` ‶
\` ‷
\frac ¼
\frac ½
\frac ¾
\frac ⅓
\frac ⅔
\frac ⅕
\frac ⅖
\frac ⅗
\frac ⅘
\frac ⅙
\frac ⅚
\frac ⅛
\frac ⅜
\frac ⅝
\frac ⅞
\frac ⅟
\bu •
\bu ◦
\bu ‣
\bu ⁌
\bu ⁍
\bub •
\buw ◦
\but ‣
\note ♩
\note ♪
\note ♫
\note ♬
\b ♭
\# ♯
\\ \
\en –
\em —
\!! ‼
\?? ⁇
\?! ‽
\?! ⁈
\!? ⁉
\die ⚀
\die ⚁
\die ⚂
\die ⚃
\die ⚄
\die ⚅
\asterisk ⁎
\asterisk ⁑
\asterisk ⁂
\asterisk ✢
\asterisk ✣
\asterisk ✤
\asterisk ✥
\asterisk ✱
\asterisk ✲
\asterisk ✳
\asterisk ✺
\asterisk ✻
\asterisk ✼
\asterisk ✽
\asterisk ❃
\asterisk ❉
\asterisk ❊
\asterisk ❋
\8< ✂
\8< ✄
\tie ⁀
\undertie ‿
\apl ⌶
\apl ⌷
\apl ⌸
\apl ⌹
\apl ⌺
\apl ⌻
\apl ⌼
\apl ⌽
\apl ⌾
\apl ⌿
\apl ⍀
\apl ⍁
\apl ⍂
\apl ⍃
\apl ⍄
\apl ⍅
\apl ⍆
\apl ⍇
\apl ⍈
\apl 

\apl ⍉
\apl ⍊
\apl ⍋
\apl ⍌
\apl ⍍
\apl ⍎
\apl ⍏
\apl ⍐
\apl ⍑
\apl ⍒
\apl ⍓
\apl ⍔
\apl ⍕
\apl ⍖
\apl ⍗
\apl ⍘
\apl ⍙
\apl ⍚
\apl ⍛
\apl 

\apl ⍜
\apl ⍝
\apl ⍞
\apl ⍟
\apl ⍠
\apl ⍡
\apl ⍢
\apl ⍣
\apl ⍤
\apl ⍥
\apl ⍦
\apl ⍧
\apl ⍨
\apl ⍩
\apl ⍪
\apl ⍫
\apl ⍬
\apl ⍭
\apl ⍮
\apl 

\apl ⍯
\apl ⍰
\apl ⍱
\apl ⍲
\apl ⍳
\apl ⍴
\apl ⍵
\apl ⍶
\apl ⍷
\apl ⍸
\apl ⍹
\apl ⍺
\apl ⎕
\^-- ̅
\^-- ̿
\_-- ̲
\_-- ̳
\^~ ̃
\^~ ͌
\_~ ̰
\^. ̇
\^. ̈
\^. ⃛
\^. ⃜
\_. ̣
\_. ̤
\^l ⃖
\^l ⃐
\^l ⃔
\^l- ⃖
\^r ⃗
\^r ⃑
\^r ⃕
\^r- ⃗
\^lr ⃡
\_lr ͍
\^^ ̂
\^^ ̑
\^^ ͆
\_^ ̭
\_^ ̯
\_^ ̪
\^v ̌
\^v ̆
\_v ̬
\_v ̮
\_v ̺
\Ga α
\GA Α
\Gb β
\GB Β
\Gg γ
\GG Γ
\Gd δ
\GD Δ
\Ge ε
\GE Ε
\Gz ζ
\GZ Ζ
\Gh η
\GH Η
\Gth θ
\GTH Θ
\Gi ι
\GI Ι
\Gk κ
\GK Κ
\Gl λ
\GL Λ
\Gl- ƛ
\Gm μ
\GM Μ
\Gn ν
\GN Ν
\Gx ξ
\GX Ξ
\Gr ρ
\GR Ρ
\Gs σ
\GS Σ
\Gt τ
\GT Τ
\Gu υ
\GU Υ
\Gf φ
\GF Φ
\Gc χ
\GC Χ
\Gp ψ
\GP Ψ
\Go ω
\GO Ω
\MiA 𝐴
\MiB 𝐵
\MiC 𝐶
\MiD 𝐷
\MiE 𝐸
\MiF 𝐹
\MiG 𝐺
\MiH 𝐻
\MiI 𝐼
\MiJ 𝐽
\MiK 𝐾
\MiL 𝐿
\MiM 𝑀
\MiN 𝑁
\MiO 𝑂
\MiP 𝑃
\MiQ 𝑄
\MiR 𝑅
\MiS 𝑆
\MiT 𝑇
\MiU 𝑈
\MiV 𝑉
\MiW 𝑊
\MiX 𝑋
\MiY 𝑌
\MiZ 𝑍
\Mia 𝑎
\Mib 𝑏
\Mic 𝑐
\Mid 𝑑
\Mie 𝑒
\Mif 𝑓
\Mig 𝑔
\Mih ℎ
\Mii 𝑖
\Mij 𝑗
\Mik 𝑘
\Mil 𝑙
\Mim 𝑚
\Min 𝑛
\Mio 𝑜
\Mip 𝑝
\Miq 𝑞
\Mir 𝑟
\Mis 𝑠
\Mit 𝑡
\Miu 𝑢
\Miv 𝑣
\Miw 𝑤
\Mix 𝑥
\Miy 𝑦
\Miz 𝑧
\MIA 𝑨
\MIB 𝑩
\MIC 𝑪
\MID 𝑫
\MIE 𝑬
\MIF 𝑭
\MIG 𝑮
\MIH 𝑯
\MII 𝑰
\MIJ 𝑱
\MIK 𝑲
\MIL 𝑳
\MIM 𝑴
\MIN 𝑵
\MIO 𝑶
\MIP 𝑷
\MIQ 𝑸
\MIR 𝑹
\MIS 𝑺
\MIT 𝑻
\MIU 𝑼
\MIV 𝑽
\MIW 𝑾
\MIX 𝑿
\MIY 𝒀
\MIZ 𝒁
\MIa 𝒂
\MIb 𝒃
\MIc 𝒄
\MId 𝒅
\MIe 𝒆
\MIf 𝒇
\MIg 𝒈
\MIh 𝒉
\MIi 𝒊
\MIj 𝒋
\MIk 𝒌
\MIl 𝒍
\MIm 𝒎
\MIn 𝒏
\MIo 𝒐
\MIp 𝒑
\MIq 𝒒
\MIr 𝒓
\MIs 𝒔
\MIt 𝒕
\MIu 𝒖
\MIv 𝒗
\MIw 𝒘
\MIx 𝒙
\MIy 𝒚
\MIz 𝒛
\McA 𝒜
\McB ℬ
\McC 𝒞
\McD 𝒟
\McE ℰ
\McF ℱ
\McG 𝒢
\McH ℋ
\McI ℐ
\McJ 𝒥
\McK 𝒦
\McL ℒ
\McM ℳ
\McN 𝒩
\McO 𝒪
\McP 𝒫
\McQ 𝒬
\McR ℛ
\McS 𝒮
\McT 𝒯
\McU 𝒰
\McV 𝒱
\McW 𝒲
\McX 𝒳
\McY 𝒴
\McZ 𝒵
\Mca 𝒶
\Mcb 𝒷
\Mcc 𝒸
\Mcd 𝒹
\Mce ℯ
\Mcf 𝒻
\Mcg ℊ
\Mch 𝒽
\Mci 𝒾
\Mcj 𝒿
\Mck 𝓀
\Mcl 𝓁
\Mcm 𝓂
\Mcn 𝓃
\Mco ℴ
\Mcp 𝓅
\Mcq 𝓆
\Mcr 𝓇
\Mcs 𝓈
\Mct 𝓉
\Mcu 𝓊
\Mcv 𝓋
\Mcw 𝓌
\Mcx 𝓍
\Mcy 𝓎
\Mcz 𝓏
\MCA 𝓐
\MCB 𝓑
\MCC 𝓒
\MCD 𝓓
\MCE 𝓔
\MCF 𝓕
\MCG 𝓖
\MCH 𝓗
\MCI 𝓘
\MCJ 𝓙
\MCK 𝓚
\MCL 𝓛
\MCM 𝓜
\MCN 𝓝
\MCO 𝓞
\MCP 𝓟
\MCQ 𝓠
\MCR 𝓡
\MCS 𝓢
\MCT 𝓣
\MCU 𝓤
\MCV 𝓥
\MCW 𝓦
\MCX 𝓧
\MCY 𝓨
\MCZ 𝓩
\MCa 𝓪
\MCb 𝓫
\MCc 𝓬
\MCd 𝓭
\MCe 𝓮
\MCf 𝓯
\MCg 𝓰
\MCh 𝓱
\MCi 𝓲
\MCj 𝓳
\MCk 𝓴
\MCl 𝓵
\MCm 𝓶
\MCn 𝓷
\MCo 𝓸
\MCp 𝓹
\MCq 𝓺
\MCr 𝓻
\MCs 𝓼
\MCt 𝓽
\MCu 𝓾
\MCv 𝓿
\MCw 𝔀
\MCx 𝔁
\MCy 𝔂
\MCz 𝔃
\MfA 𝔄
\MfB 𝔅
\MfC ℭ
\MfD 𝔇
\MfE 𝔈
\MfF 𝔉
\MfG 𝔊
\MfH ℌ
\MfI ℑ
\MfJ 𝔍
\MfK 𝔎
\MfL 𝔏
\MfM 𝔐
\MfN 𝔑
\MfO 𝔒
\MfP 𝔓
\MfQ 𝔔
\MfR ℜ
\MfS 𝔖
\MfT 𝔗
\MfU 𝔘
\MfV 𝔙
\MfW 𝔚
\MfX 𝔛
\MfY 𝔜
\MfZ ℨ
\Mfa 𝔞
\Mfb 𝔟
\Mfc 𝔠
\Mfd 𝔡
\Mfe 𝔢
\Mff 𝔣
\Mfg 𝔤
\Mfh 𝔥
\Mfi 𝔦
\Mfj 𝔧
\Mfk 𝔨
\Mfl 𝔩
\Mfm 𝔪
\Mfn 𝔫
\Mfo 𝔬
\Mfp 𝔭
\Mfq 𝔮
\Mfr 𝔯
\Mfs 𝔰
\Mft 𝔱
\Mfu 𝔲
\Mfv 𝔳
\Mfw 𝔴
\Mfx 𝔵
\Mfy 𝔶
\Mfz 𝔷
\_a ₐ
\_e ₑ
\_h ₕ
\_i ᵢ
\_j ⱼ
\_k ₖ
\_l ₗ
\_m ₘ
\_n ₙ
\_o ₒ
\_p ₚ
\_r ᵣ
\_s ₛ
\_t ₜ
\_u ᵤ
\_v ᵥ
\_x ₓ
\_Gb ᵦ
\_Gg ᵧ
\_Gr ᵨ
\_Gf ᵩ
\_Gc ᵪ
\^a ᵃ
\^b ᵇ
\^c ᶜ
\^d ᵈ
\^e ᵉ
\^f ᶠ
\^g ᵍ
\^h ʰ
\^i ⁱ
\^j ʲ
\^k ᵏ
\^l ˡ
\^m ᵐ
\^n ⁿ
\^o ᵒ
\^p ᵖ
\^r ʳ
\^s ˢ
\^t ᵗ
\^u ᵘ
\^v ᵛ
\^w ʷ
\^x ˣ
\^y ʸ
\^z ᶻ
\^A ᴬ
\^B ᴮ
\^D ᴰ
\^E ᴱ
\^G ᴳ
\^H ᴴ
\^I ᴵ
\^J ᴶ
\^K ᴷ
\^L ᴸ
\^M ᴹ
\^N ᴺ
\^O ᴼ
\^P ᴾ
\^R ᴿ
\^T ᵀ
\^U ᵁ
\^V ⱽ
\^W ᵂ
\^Gb ᵝ
\^Gg ᵞ
\^Gd ᵟ
\^Ge ᵋ
\^Gth ᶿ
\^Gf ᵠ
\^Gc ᵡ
\   
\! ¡
\cent ¢
\brokenbar ¦
\degree °
\? ¿
\^a_ ª
\^o_ º
\(0) ⓪
\(0) 🄀
\(0) ⓿
\(0) 🄋
\(0) 🄌
\(1) ⑴
\(1) ①
\(1) ⒈
\(1) ❶
\(1) ➀
\(1) ➊
\(2) ⑵
\(2) ②
\(2) ⒉
\(2) ❷
\(2) ➁
\(2) ➋
\(3) ⑶
\(3) ③
\(3) ⒊
\(3) ❸
\(3) ➂
\(3) ➌
\(4) ⑷
\(4) ④
\(4) ⒋
\(4) ❹
\(4) ➃
\(4) ➍
\(5) ⑸
\(5) ⑤
\(5) ⒌
\(5) ❺
\(5) ➄
\(5) ➎
\(6) ⑹
\(6) ⑥
\(6) ⒍
\(6) ❻
\(6) ➅
\(6) ➏
\(7) ⑺
\(7) ⑦
\(7) ⒎
\(7) ❼
\(7) ➆
\(7) ➐
\(8) ⑻
\(8) ⑧
\(8) ⒏
\(8) ❽
\(8) ➇
\(8) ➑
\(9) ⑼
\(9) ⑨
\(9) ⒐
\(9) ❾
\(9) ➈
\(9) ➒
\(10) ⑽
\(10) ⑩
\(10) ⒑
\(10) ❿
\(10) ➉
\(10) ➓
\(11) ⑾
\(11) ⑪
\(11) ⒒
\(11) ⓫
\(12) ⑿
\(12) ⑫
\(12) ⒓
\(12) ⓬
\(13) ⒀
\(13) ⑬
\(13) ⒔
\(13) ⓭
\(14) ⒁
\(14) ⑭
\(14) ⒕
\(14) ⓮
\(15) ⒂
\(15) ⑮
\(15) ⒖
\(15) ⓯
\(16) ⒃
\(16) ⑯
\(16) ⒗
\(16) ⓰
\(17) ⒄
\(17) ⑰
\(17) ⒘
\(17) ⓱
\(18) ⒅
\(18) ⑱
\(18) ⒙
\(18) ⓲
\(19) ⒆
\(19) ⑲
\(19) ⒚
\(19) ⓳
\(20) ⒇
\(20) ⑳
\(20) ⒛
\(20) ⓴
\(a) ⒜
\(a) Ⓐ
\(a) ⓐ
\(a) 🅐
\(a) 🄰
\(a) 🅰
\(b) ⒝
\(b) Ⓑ
\(b) ⓑ
\(b) 🅑
\(b) 🄱
\(b) 🅱
\(c) ⒞
\(c) Ⓒ
\(c) ⓒ
\(c) 🅒
\(c) 🄲
\(c) 🅲
\(d) ⒟
\(d) Ⓓ
\(d) ⓓ
\(d) 🅓
\(d) 🄳
\(d) 🅳
\(e) ⒠
\(e) Ⓔ
\(e) ⓔ
\(e) 🅔
\(e) 🄴
\(e) 🅴
\(f) ⒡
\(f) Ⓕ
\(f) ⓕ
\(f) 🅕
\(f) 🄵
\(f) 🅵
\(g) ⒢
\(g) Ⓖ
\(g) ⓖ
\(g) 🅖
\(g) 🄶
\(g) 🅶
\(h) ⒣
\(h) Ⓗ
\(h) ⓗ
\(h) 🅗
\(h) 🄷
\(h) 🅷
\(i) ⒤
\(i) Ⓘ
\(i) ⓘ
\(i) 🅘
\(i) 🄸
\(i) 🅸
\(j) ⒥
\(j) Ⓙ
\(j) ⓙ
\(j) 🅙
\(j) 🄹
\(j) 🅹
\(k) ⒦
\(k) Ⓚ
\(k) ⓚ
\(k) 🅚
\(k) 🄺
\(k) 🅺
\(l) ⒧
\(l) Ⓛ
\(l) ⓛ
\(l) 🅛
\(l) 🄻
\(l) 🅻
\(m) ⒨
\(m) Ⓜ
\(m) ⓜ
\(m) 🅜
\(m) 🄼
\(m) 🅼
\(n) ⒩
\(n) Ⓝ
\(n) ⓝ
\(n) 🅝
\(n) 🄽
\(n) 🅽
\(o) ⒪
\(o) Ⓞ
\(o) ⓞ
\(o) 🅞
\(o) 🄾
\(o) 🅾
\(p) ⒫
\(p) Ⓟ
\(p) ⓟ
\(p) 🅟
\(p) 🄿
\(p) 🅿
\(q) ⒬
\(q) Ⓠ
\(q) ⓠ
\(q) 🅠
\(q) 🅀
\(q) 🆀
\(r) ⒭
\(r) Ⓡ
\(r) ⓡ
\(r) 🅡
\(r) 🅁
\(r) 🆁
\(s) ⒮
\(s) Ⓢ
\(s) ⓢ
\(s) 🅢
\(s) 🅂
\(s) 🆂
\(t) ⒯
\(t) Ⓣ
\(t) ⓣ
\(t) 🅣
\(t) 🅃
\(t) 🆃
\(u) ⒰
\(u) Ⓤ
\(u) ⓤ
\(u) 🅤
\(u) 🅄
\(u) 🆄
\(v) ⒱
\(v) Ⓥ
\(v) ⓥ
\(v) 🅥
\(v) 🅅
\(v) 🆅
\(w) ⒲
\(w) Ⓦ
\(w) ⓦ
\(w) 🅦
\(w) 🅆
\(w) 🆆
\(x) ⒳
\(x) Ⓧ
\(x) ⓧ
\(x) 🅧
\(x) 🅇
\(x) 🆇
\(y) ⒴
\(y) Ⓨ
\(y) ⓨ
\(y) 🅨
\(y) 🅈
\(y) 🆈
\(z) ⒵
\(z) Ⓩ
\(z) ⓩ
\(z) 🅩
\(z) 🅉
\(z) 🆉

Gen.hs

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wall #-}

module Gen where

import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.Text.IO as T
import Data.Void (Void)
import Text.Megaparsec
import Text.Megaparsec.Char
import qualified Text.Megaparsec.Char.Lexer as L

type QuickPhraseEntry = (Text, Text)

type QuickPhrase = [(Text, Text)]

type Parser = Parsec Void Text

type Translation = (Text, [Text])

stringLiteral :: Parser Text
stringLiteral = T.pack <$> (char '"' >> manyTill L.charLiteral (char '"'))

symbol :: Text -> Parser Text
symbol = L.symbol space

parens :: Parser a -> Parser a
parens = between (symbol "(") (symbol ")")

dot :: Parser Text
dot = symbol "."

comma :: Parser Text
comma = symbol ","

output1 :: Parser [Text]
output1 = (\xs -> [c | (T.singleton -> c) <- T.unpack xs, c /= " "]) <$> (comma >> parens ("agda-input-to-string-list" >> space >> stringLiteral))

output2 :: Parser [Text]
output2 = parens (stringLiteral `sepBy` space)

translation :: Parser Translation
translation = parens $ do
  key <- stringLiteral
  _ <- space
  _ <- dot
  _ <- space
  output <- output1 <|> output2
  pure (key, output)

mySpace :: Parser ()
mySpace = L.space space1 (L.skipLineComment ";;") empty

translations :: Parser [Translation]
translations = optional mySpace >> (translation `sepEndBy` mySpace) <* eof

toQuickPhrase :: [(Text, [Text])] -> QuickPhrase
toQuickPhrase xs = [("\\" <> key, phrase) | (key, ys) <- xs, phrase <- ys]

writeQuickPhrase :: FilePath -> QuickPhrase -> IO ()
writeQuickPhrase fp = T.writeFile fp . T.unlines . ls
  where
    ls = map $ \(key, phrase) -> key <> " " <> phrase

main :: IO ()
main = do
  content <- T.readFile "input.txt"
  case parse translations "" content of
    Right (toQuickPhrase -> qp) -> writeQuickPhrase "agda.mb" qp
    Left err -> putStrLn $ errorBundlePretty err