Skip to content
Snippets Groups Projects
Commit 5d023ba4 authored by Ralf Jung's avatar Ralf Jung
Browse files

move some lengthy unicode configurations to separate files

parent 04aa50f6
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
docs/editor.md
+ 3
− 312
View file @ 5d023ba4
......@@ -183,134 +183,7 @@ On Linux with old versions of CoqIDE you can use the Intelligent
Input Bus (IBus) framework to input Unicode symbols. First, install `ibus-m17n`
via your system's package manager. Next, create a file `~/.m17n.d/coq.mim` to
configure an input method based on the math symbol list, and with some custom
aliases for symbols used a lot in Iris:
```
;; Usage: copy to ~/.m17n.d/coq.mim
(input-method t coq)
(description "Input method for Coq")
(title "Coq")
(map (trans
;; Standard LaTeX math notations
("\\forall" "∀")
("\\exists" "∃")
("\\lam" "λ")
("\\not" "¬")
("\\/" "∨")
("/\\" "∧")
("->" "→")
("<->" "↔")
("\\<-" "←") ;; we add a backslash because the plain <- is used for the rewrite tactic
("\\==" "≡")
("\\/==" "≢")
("/=" "≠")
("<=" "≤")
("\\in" "∈")
("\\notin" "∉")
("\\cup" "∪")
("\\cap" "∩")
("\\setminus" "∖")
("\\subset" "⊂")
("\\subseteq" "⊆")
("\\sqsubseteq" "⊑")
("\\sqsubseteq" "⊑")
("\\notsubseteq" "⊈")
("\\meet" "⊓")
("\\join" "⊔")
("\\top" "⊤")
("\\bottom" "⊥")
("\\vdash" "⊢")
("\\dashv" "⊣")
("\\Vdash" "⊨")
("\\infty" "∞")
("\\comp" "∘")
("\\prf" "↾")
("\\bind" "≫=")
("\\mapsto" "↦")
("\\hookrightarrow" "↪")
("\\uparrow" "↑")
;; Iris specific
("\\fun" "λ")
("\\mult" "⋅")
("\\ent" "⊢")
("\\valid" "✓")
("\\diamond" "◇")
("\\box" "□")
("\\bbox" "■")
("\\later" "▷")
("\\pred" "φ")
("\\and" "∧")
("\\or" "∨")
("\\comp" "∘")
("\\ccomp" "◎")
("\\all" "∀")
("\\ex" "∃")
("\\to" "→")
("\\sep" "∗")
("\\lc" "⌜")
("\\rc" "⌝")
("\\Lc" "⎡")
("\\Rc" "⎤")
("\\empty" "∅")
("\\Lam" "Λ")
("\\Sig" "Σ")
("\\-" "∖")
("\\aa" "●")
("\\af" "◯")
("\\auth" "●")
("\\frag" "◯")
("\\iff" "↔")
("\\gname" "γ")
("\\incl" "≼")
("\\latert" "▶")
("\\update" "⇝")
("\\bind" "≫=")
;; accents (for iLöb)
("\\\"o" "ö")
;; subscripts and superscripts
("^^+" "⁺") ("__+" "₊") ("^^-" "⁻")
("__0" "₀") ("__1" "₁") ("__2" "₂") ("__3" "₃") ("__4" "₄")
("__5" "₅") ("__6" "₆") ("__7" "₇") ("__8" "₈") ("__9" "₉")
("__a" "ₐ") ("__e" "ₑ") ("__h" "ₕ") ("__i" "ᵢ") ("__k" "ₖ")
("__l" "ₗ") ("__m" "ₘ") ("__n" "ₙ") ("__o" "ₒ") ("__p" "ₚ")
("__r" "ᵣ") ("__s" "ₛ") ("__t" "ₜ") ("__u" "ᵤ") ("__v" "ᵥ") ("__x" "ₓ")
;; Greek alphabet
("\\Alpha" "Α") ("\\alpha" "α")
("\\Beta" "Β") ("\\beta" "β")
("\\Gamma" "Γ") ("\\gamma" "γ")
("\\Delta" "Δ") ("\\delta" "δ")
("\\Epsilon" "Ε") ("\\epsilon" "ε")
("\\Zeta" "Ζ") ("\\zeta" "ζ")
("\\Eta" "Η") ("\\eta" "η")
("\\Theta" "Θ") ("\\theta" "θ")
("\\Iota" "Ι") ("\\iota" "ι")
("\\Kappa" "Κ") ("\\kappa" "κ")
("\\Lamda" "Λ") ("\\lamda" "λ")
("\\Lambda" "Λ") ("\\lambda" "λ")
("\\Mu" "Μ") ("\\mu" "μ")
("\\Nu" "Ν") ("\\nu" "ν")
("\\Xi" "Ξ") ("\\xi" "ξ")
("\\Omicron" "Ο") ("\\omicron" "ο")
("\\Pi" "Π") ("\\pi" "π")
("\\Rho" "Ρ") ("\\rho" "ρ")
("\\Sigma" "Σ") ("\\sigma" "σ")
("\\Tau" "Τ") ("\\tau" "τ")
("\\Upsilon" "Υ") ("\\upsilon" "υ")
("\\Phi" "Φ") ("\\phi" "φ")
("\\Chi" "Χ") ("\\chi" "χ")
("\\Psi" "Ψ") ("\\psi" "ψ")
("\\Omega" "Ω") ("\\omega" "ω")
))
(state (init (trans)))
```
aliases for symbols used a lot in Iris as defined [here](ibus).
To use this input method, you should:
......@@ -435,189 +308,7 @@ extension](https://marketplace.visualstudio.com/items?itemName=mr-konn.generic-i
To insert a symbol, type the code for a symbol such as `\to` and then press
`Space` or `Tab`. To enable Iris unicode input support, open your user settings,
press `Cmd ,` or `Ctrl ,`, type "generic-input-methods.input-methods", and then
click on "Edit in settings.json" and add the following:
```
"generic-input-methods.input-methods": [
{
"name": "Iris Math",
"commandName": "text.math",
"languages": [
"coq"
],
"triggers": [
"\\"
],
"dictionary": [
// Standard LaTeX math notations
{ "label": "forall", "body": "∀", "description": "∀" },
{ "label": "exists", "body": "∃", "description": "∃" },
{ "label": "lam", "body": "λ", "description": "λ" },
{ "label": "not", "body": "¬", "description": "¬" },
{ "label": "->", "body": "→", "description": "→" },
{ "label": "<->", "body": "↔", "description": "↔" },
{ "label": "<-", "body": "←", "description": "←" },
{ "label": "==", "body": "≡", "description": "≡" },
{ "label": "/==", "body": "≢", "description": "≢" },
{ "label": "/=", "body": "≠", "description": "≠" },
{ "label": "neq", "body": "≠", "description": "≠" },
{ "label": "nequiv", "body": "≢", "description": "≢" },
{ "label": "<=", "body": "≤", "description": "≤" },
{ "label": "leq", "body": "≤", "description": "≤" },
{ "label": "in", "body": "∈", "description": "∈" },
{ "label": "notin", "body": "∉", "description": "∉" },
{ "label": "cup", "body": "∪", "description": "∪" },
{ "label": "cap", "body": "∩", "description": "∩" },
{ "label": "setminus", "body": "∖", "description": "∖" },
{ "label": "subset", "body": "⊂", "description": "⊂" },
{ "label": "subseteq", "body": "⊆", "description": "⊆" },
{ "label": "sqsubseteq", "body": "⊑", "description": "⊑" },
{ "label": "sqsubseteq", "body": "⊑", "description": "⊑" },
{ "label": "notsubseteq", "body": "⊈", "description": "⊈" },
{ "label": "meet", "body": "⊓", "description": "⊓" },
{ "label": "join", "body": "⊔", "description": "⊔" },
{ "label": "top", "body": "⊤", "description": "⊤" },
{ "label": "bottom", "body": "⊥", "description": "⊥" },
{ "label": "vdash", "body": "⊢", "description": "⊢" },
{ "label": "|-", "body": "⊢", "description": "⊢" },
{ "label": "dashv", "body": "⊣", "description": "⊣" },
{ "label": "Vdash", "body": "⊨", "description": "⊨" },
{ "label": "infty", "body": "∞", "description": "∞" },
{ "label": "comp", "body": "∘", "description": "∘" },
{ "label": "prf", "body": "↾", "description": "↾" },
{ "label": "bind", "body": "≫=", "description": "≫=" },
{ "label": "mapsto", "body": "↦", "description": "↦" },
{ "label": "hookrightarrow", "body": "↪", "description": "↪" },
{ "label": "uparrow", "body": "↑", "description": "↑" },
// Iris specific
{ "label": "fun", "body": "λ", "description": "λ" },
{ "label": "mult", "body": "⋅", "description": "⋅" },
{ "label": "ent", "body": "⊢", "description": "⊢" },
{ "label": "valid", "body": "✓", "description": "✓" },
{ "label": "diamond", "body": "◇", "description": "◇" },
{ "label": "box", "body": "□", "description": "□" },
{ "label": "bbox", "body": "■", "description": "■" },
{ "label": "later", "body": "▷", "description": "▷" },
{ "label": "pred", "body": "φ", "description": "φ" },
{ "label": "and", "body": "∧", "description": "∧" },
{ "label": "or", "body": "∨", "description": "∨" },
{ "label": "comp", "body": "∘", "description": "∘" },
{ "label": "ccomp", "body": "◎", "description": "◎" },
{ "label": "all", "body": "∀", "description": "∀" },
{ "label": "ex", "body": "∃", "description": "∃" },
{ "label": "to", "body": "→", "description": "→" },
{ "label": "sep", "body": "∗", "description": "∗" },
{ "label": "star", "body": "∗", "description": "∗" },
{ "label": "lc", "body": "⌜", "description": "⌜" },
{ "label": "rc", "body": "⌝", "description": "⌝" },
{ "label": "Lc", "body": "⎡", "description": "⎡" },
{ "label": "Rc", "body": "⎤", "description": "⎤" },
{ "label": "empty", "body": "∅", "description": "∅" },
{ "label": "Lam", "body": "Λ", "description": "Λ" },
{ "label": "Sig", "body": "Σ", "description": "Σ" },
{ "label": "-", "body": "∖", "description": "∖" },
{ "label": "aa", "body": "●", "description": "●" },
{ "label": "af", "body": "◯", "description": "◯" },
{ "label": "auth", "body": "●", "description": "●" },
{ "label": "frag", "body": "◯", "description": "◯" },
{ "label": "iff", "body": "↔", "description": "↔" },
{ "label": "gname", "body": "γ", "description": "γ" },
{ "label": "incl", "body": "≼", "description": "≼" },
{ "label": "latert", "body": "▶", "description": "▶" },
{ "label": "update", "body": "⇝", "description": "⇝" },
{ "label": "bind", "body": "≫=", "description": "≫=" },
// accents (for iLöb)
{ "label": "\"o", "body": "ö", "description": "ö" },
// subscripts and superscripts
{ "label": "^^+", "body": "⁺", "description": "⁺" },
{ "label": "__+", "body": "₊", "description": "₊" },
{ "label": "^^-", "body": "⁻", "description": "⁻" },
{ "label": "__0", "body": "₀", "description": "₀" },
{ "label": "__1", "body": "₁", "description": "₁" },
{ "label": "__2", "body": "₂", "description": "₂" },
{ "label": "__3", "body": "₃", "description": "₃" },
{ "label": "__4", "body": "₄", "description": "₄" },
{ "label": "__5", "body": "₅", "description": "₅" },
{ "label": "__6", "body": "₆", "description": "₆" },
{ "label": "__7", "body": "₇", "description": "₇" },
{ "label": "__8", "body": "₈", "description": "₈" },
{ "label": "__9", "body": "₉", "description": "₉" },
{ "label": "__a", "body": "ₐ", "description": "ₐ" },
{ "label": "__e", "body": "ₑ", "description": "ₑ" },
{ "label": "__h", "body": "ₕ", "description": "ₕ" },
{ "label": "__i", "body": "ᵢ", "description": "ᵢ" },
{ "label": "__k", "body": "ₖ", "description": "ₖ" },
{ "label": "__l", "body": "ₗ", "description": "ₗ" },
{ "label": "__m", "body": "ₘ", "description": "ₘ" },
{ "label": "__n", "body": "ₙ", "description": "ₙ" },
{ "label": "__o", "body": "ₒ", "description": "ₒ" },
{ "label": "__p", "body": "ₚ", "description": "ₚ" },
{ "label": "__r", "body": "ᵣ", "description": "ᵣ" },
{ "label": "__s", "body": "ₛ", "description": "ₛ" },
{ "label": "__t", "body": "ₜ", "description": "ₜ" },
{ "label": "__u", "body": "ᵤ", "description": "ᵤ" },
{ "label": "__v", "body": "ᵥ", "description": "ᵥ" },
{ "label": "__x", "body": "ₓ", "description": "ₓ" },
// Greek alphabet
{ "label": "Alpha", "body": "Α", "description": "Α" },
{ "label": "alpha", "body": "α", "description": "α" },
{ "label": "Beta", "body": "Β", "description": "Β" },
{ "label": "beta", "body": "β", "description": "β" },
{ "label": "Gamma", "body": "Γ", "description": "Γ" },
{ "label": "gamma", "body": "γ", "description": "γ" },
{ "label": "Delta", "body": "Δ", "description": "Δ" },
{ "label": "delta", "body": "δ", "description": "δ" },
{ "label": "Epsilon", "body": "Ε", "description": "Ε" },
{ "label": "epsilon", "body": "ε", "description": "ε" },
{ "label": "Zeta", "body": "Ζ", "description": "Ζ" },
{ "label": "zeta", "body": "ζ", "description": "ζ" },
{ "label": "Eta", "body": "Η", "description": "Η" },
{ "label": "eta", "body": "η", "description": "η" },
{ "label": "Theta", "body": "Θ", "description": "Θ" },
{ "label": "theta", "body": "θ", "description": "θ" },
{ "label": "Iota", "body": "Ι", "description": "Ι" },
{ "label": "iota", "body": "ι", "description": "ι" },
{ "label": "Kappa", "body": "Κ", "description": "Κ" },
{ "label": "kappa", "body": "κ", "description": "κ" },
{ "label": "Lamda", "body": "Λ", "description": "Λ" },
{ "label": "lamda", "body": "λ", "description": "λ" },
{ "label": "Lambda", "body": "Λ", "description": "Λ" },
{ "label": "lambda", "body": "λ", "description": "λ" },
{ "label": "Mu", "body": "Μ", "description": "Μ" },
{ "label": "mu", "body": "μ", "description": "μ" },
{ "label": "Nu", "body": "Ν", "description": "Ν" },
{ "label": "nu", "body": "ν", "description": "ν" },
{ "label": "Xi", "body": "Ξ", "description": "Ξ" },
{ "label": "xi", "body": "ξ", "description": "ξ" },
{ "label": "Omicron", "body": "Ο", "description": "Ο" },
{ "label": "omicron", "body": "ο", "description": "ο" },
{ "label": "Pi", "body": "Π", "description": "Π" },
{ "label": "pi", "body": "π", "description": "π" },
{ "label": "Rho", "body": "Ρ", "description": "Ρ" },
{ "label": "rho", "body": "ρ", "description": "ρ" },
{ "label": "Sigma", "body": "Σ", "description": "Σ" },
{ "label": "sigma", "body": "σ", "description": "σ" },
{ "label": "Tau", "body": "Τ", "description": "Τ" },
{ "label": "tau", "body": "τ", "description": "τ" },
{ "label": "Upsilon", "body": "Υ", "description": "Υ" },
{ "label": "upsilon", "body": "υ", "description": "υ" },
{ "label": "Phi", "body": "Φ", "description": "Φ" },
{ "label": "phi", "body": "φ", "description": "φ" },
{ "label": "Chi", "body": "Χ", "description": "Χ" },
{ "label": "chi", "body": "χ", "description": "χ" },
{ "label": "Psi", "body": "Ψ", "description": "Ψ" },
{ "label": "psi", "body": "ψ", "description": "ψ" },
{ "label": "Omega", "body": "Ω", "description": "Ω" },
{ "label": "omega", "body": "ω", "description": "ω" }
]
}
]
```
click on "Edit in settings.json" and add the contents of [this file](vscode).
## Vim
......@@ -698,4 +389,4 @@ let g:UltiSnipsExpandTrigger="<c-l>"
```
To insert a unicode character, type its trigger word, such as `\forall` or `->`, and then press `<c-l>` while still in insert mode.
To register most common unicode characters, put [this file](/docs/vim_ultisnips) either at `~/.vim/UltiSnips/coq_unicode.snippets` or `~/.config/nvim/UltiSnips/coq_unicode.snippets`, depending on your preferred variant of Vim.
To register most common unicode characters, put [this file](vim_ultisnips) either at `~/.vim/UltiSnips/coq_unicode.snippets` or `~/.config/nvim/UltiSnips/coq_unicode.snippets`, depending on your preferred variant of Vim.
docs/ibus 0 → 100644
+ 124
− 0
View file @ 5d023ba4
;; Usage: copy to ~/.m17n.d/coq.mim
(input-method t coq)
(description "Input method for Coq")
(title "Coq")
(map (trans
;; Standard LaTeX math notations
("\\forall" "∀")
("\\exists" "∃")
("\\lam" "λ")
("\\not" "¬")
("\\/" "∨")
("/\\" "∧")
("->" "→")
("<->" "↔")
("\\<-" "←") ;; we add a backslash because the plain <- is used for the rewrite tactic
("\\==" "≡")
("\\/==" "≢")
("/=" "≠")
("<=" "≤")
("\\in" "∈")
("\\notin" "∉")
("\\cup" "∪")
("\\cap" "∩")
("\\setminus" "∖")
("\\subset" "⊂")
("\\subseteq" "⊆")
("\\sqsubseteq" "⊑")
("\\sqsubseteq" "⊑")
("\\notsubseteq" "⊈")
("\\meet" "⊓")
("\\join" "⊔")
("\\top" "⊤")
("\\bottom" "⊥")
("\\vdash" "⊢")
("\\dashv" "⊣")
("\\Vdash" "⊨")
("\\infty" "∞")
("\\comp" "∘")
("\\prf" "↾")
("\\bind" "≫=")
("\\mapsto" "↦")
("\\hookrightarrow" "↪")
("\\uparrow" "↑")
;; Iris specific
("\\fun" "λ")
("\\mult" "⋅")
("\\ent" "⊢")
("\\valid" "✓")
("\\diamond" "◇")
("\\box" "□")
("\\bbox" "■")
("\\later" "▷")
("\\pred" "φ")
("\\and" "∧")
("\\or" "∨")
("\\comp" "∘")
("\\ccomp" "◎")
("\\all" "∀")
("\\ex" "∃")
("\\to" "→")
("\\sep" "∗")
("\\lc" "⌜")
("\\rc" "⌝")
("\\Lc" "⎡")
("\\Rc" "⎤")
("\\empty" "∅")
("\\Lam" "Λ")
("\\Sig" "Σ")
("\\-" "∖")
("\\aa" "●")
("\\af" "◯")
("\\auth" "●")
("\\frag" "◯")
("\\iff" "↔")
("\\gname" "γ")
("\\incl" "≼")
("\\latert" "▶")
("\\update" "⇝")
("\\bind" "≫=")
;; accents (for iLöb)
("\\\"o" "ö")
;; subscripts and superscripts
("^^+" "⁺") ("__+" "₊") ("^^-" "⁻")
("__0" "₀") ("__1" "₁") ("__2" "₂") ("__3" "₃") ("__4" "₄")
("__5" "₅") ("__6" "₆") ("__7" "₇") ("__8" "₈") ("__9" "₉")
("__a" "ₐ") ("__e" "ₑ") ("__h" "ₕ") ("__i" "ᵢ") ("__k" "ₖ")
("__l" "ₗ") ("__m" "ₘ") ("__n" "ₙ") ("__o" "ₒ") ("__p" "ₚ")
("__r" "ᵣ") ("__s" "ₛ") ("__t" "ₜ") ("__u" "ᵤ") ("__v" "ᵥ") ("__x" "ₓ")
;; Greek alphabet
("\\Alpha" "Α") ("\\alpha" "α")
("\\Beta" "Β") ("\\beta" "β")
("\\Gamma" "Γ") ("\\gamma" "γ")
("\\Delta" "Δ") ("\\delta" "δ")
("\\Epsilon" "Ε") ("\\epsilon" "ε")
("\\Zeta" "Ζ") ("\\zeta" "ζ")
("\\Eta" "Η") ("\\eta" "η")
("\\Theta" "Θ") ("\\theta" "θ")
("\\Iota" "Ι") ("\\iota" "ι")
("\\Kappa" "Κ") ("\\kappa" "κ")
("\\Lamda" "Λ") ("\\lamda" "λ")
("\\Lambda" "Λ") ("\\lambda" "λ")
("\\Mu" "Μ") ("\\mu" "μ")
("\\Nu" "Ν") ("\\nu" "ν")
("\\Xi" "Ξ") ("\\xi" "ξ")
("\\Omicron" "Ο") ("\\omicron" "ο")
("\\Pi" "Π") ("\\pi" "π")
("\\Rho" "Ρ") ("\\rho" "ρ")
("\\Sigma" "Σ") ("\\sigma" "σ")
("\\Tau" "Τ") ("\\tau" "τ")
("\\Upsilon" "Υ") ("\\upsilon" "υ")
("\\Phi" "Φ") ("\\phi" "φ")
("\\Chi" "Χ") ("\\chi" "χ")
("\\Psi" "Ψ") ("\\psi" "ψ")
("\\Omega" "Ω") ("\\omega" "ω")
))
(state (init (trans)))
docs/vscode 0 → 100644
+ 178
− 0
View file @ 5d023ba4
"generic-input-methods.input-methods": [
{
"name": "Iris Math",
"commandName": "text.math",
"languages": [
"coq"
],
"triggers": [
"\\"
],
"dictionary": [
// Standard LaTeX math notations
{ "label": "forall", "body": "∀", "description": "∀" },
{ "label": "exists", "body": "∃", "description": "∃" },
{ "label": "lam", "body": "λ", "description": "λ" },
{ "label": "not", "body": "¬", "description": "¬" },
{ "label": "->", "body": "→", "description": "→" },
{ "label": "<->", "body": "↔", "description": "↔" },
{ "label": "<-", "body": "←", "description": "←" },
{ "label": "==", "body": "≡", "description": "≡" },
{ "label": "/==", "body": "≢", "description": "≢" },
{ "label": "/=", "body": "≠", "description": "≠" },
{ "label": "neq", "body": "≠", "description": "≠" },
{ "label": "nequiv", "body": "≢", "description": "≢" },
{ "label": "<=", "body": "≤", "description": "≤" },
{ "label": "leq", "body": "≤", "description": "≤" },
{ "label": "in", "body": "∈", "description": "∈" },
{ "label": "notin", "body": "∉", "description": "∉" },
{ "label": "cup", "body": "∪", "description": "∪" },
{ "label": "cap", "body": "∩", "description": "∩" },
{ "label": "setminus", "body": "∖", "description": "∖" },
{ "label": "subset", "body": "⊂", "description": "⊂" },
{ "label": "subseteq", "body": "⊆", "description": "⊆" },
{ "label": "sqsubseteq", "body": "⊑", "description": "⊑" },
{ "label": "sqsubseteq", "body": "⊑", "description": "⊑" },
{ "label": "notsubseteq", "body": "⊈", "description": "⊈" },
{ "label": "meet", "body": "⊓", "description": "⊓" },
{ "label": "join", "body": "⊔", "description": "⊔" },
{ "label": "top", "body": "⊤", "description": "⊤" },
{ "label": "bottom", "body": "⊥", "description": "⊥" },
{ "label": "vdash", "body": "⊢", "description": "⊢" },
{ "label": "|-", "body": "⊢", "description": "⊢" },
{ "label": "dashv", "body": "⊣", "description": "⊣" },
{ "label": "Vdash", "body": "⊨", "description": "⊨" },
{ "label": "infty", "body": "∞", "description": "∞" },
{ "label": "comp", "body": "∘", "description": "∘" },
{ "label": "prf", "body": "↾", "description": "↾" },
{ "label": "bind", "body": "≫=", "description": "≫=" },
{ "label": "mapsto", "body": "↦", "description": "↦" },
{ "label": "hookrightarrow", "body": "↪", "description": "↪" },
{ "label": "uparrow", "body": "↑", "description": "↑" },
// Iris specific
{ "label": "fun", "body": "λ", "description": "λ" },
{ "label": "mult", "body": "⋅", "description": "⋅" },
{ "label": "ent", "body": "⊢", "description": "⊢" },
{ "label": "valid", "body": "✓", "description": "✓" },
{ "label": "diamond", "body": "◇", "description": "◇" },
{ "label": "box", "body": "□", "description": "□" },
{ "label": "bbox", "body": "■", "description": "■" },
{ "label": "later", "body": "▷", "description": "▷" },
{ "label": "pred", "body": "φ", "description": "φ" },
{ "label": "and", "body": "∧", "description": "∧" },
{ "label": "or", "body": "∨", "description": "∨" },
{ "label": "comp", "body": "∘", "description": "∘" },
{ "label": "ccomp", "body": "◎", "description": "◎" },
{ "label": "all", "body": "∀", "description": "∀" },
{ "label": "ex", "body": "∃", "description": "∃" },
{ "label": "to", "body": "→", "description": "→" },
{ "label": "sep", "body": "∗", "description": "∗" },
{ "label": "star", "body": "∗", "description": "∗" },
{ "label": "lc", "body": "⌜", "description": "⌜" },
{ "label": "rc", "body": "⌝", "description": "⌝" },
{ "label": "Lc", "body": "⎡", "description": "⎡" },
{ "label": "Rc", "body": "⎤", "description": "⎤" },
{ "label": "empty", "body": "∅", "description": "∅" },
{ "label": "Lam", "body": "Λ", "description": "Λ" },
{ "label": "Sig", "body": "Σ", "description": "Σ" },
{ "label": "-", "body": "∖", "description": "∖" },
{ "label": "aa", "body": "●", "description": "●" },
{ "label": "af", "body": "◯", "description": "◯" },
{ "label": "auth", "body": "●", "description": "●" },
{ "label": "frag", "body": "◯", "description": "◯" },
{ "label": "iff", "body": "↔", "description": "↔" },
{ "label": "gname", "body": "γ", "description": "γ" },
{ "label": "incl", "body": "≼", "description": "≼" },
{ "label": "latert", "body": "▶", "description": "▶" },
{ "label": "update", "body": "⇝", "description": "⇝" },
{ "label": "bind", "body": "≫=", "description": "≫=" },
// accents (for iLöb)
{ "label": "\"o", "body": "ö", "description": "ö" },
// subscripts and superscripts
{ "label": "^^+", "body": "⁺", "description": "⁺" },
{ "label": "__+", "body": "₊", "description": "₊" },
{ "label": "^^-", "body": "⁻", "description": "⁻" },
{ "label": "__0", "body": "₀", "description": "₀" },
{ "label": "__1", "body": "₁", "description": "₁" },
{ "label": "__2", "body": "₂", "description": "₂" },
{ "label": "__3", "body": "₃", "description": "₃" },
{ "label": "__4", "body": "₄", "description": "₄" },
{ "label": "__5", "body": "₅", "description": "₅" },
{ "label": "__6", "body": "₆", "description": "₆" },
{ "label": "__7", "body": "₇", "description": "₇" },
{ "label": "__8", "body": "₈", "description": "₈" },
{ "label": "__9", "body": "₉", "description": "₉" },
{ "label": "__a", "body": "ₐ", "description": "ₐ" },
{ "label": "__e", "body": "ₑ", "description": "ₑ" },
{ "label": "__h", "body": "ₕ", "description": "ₕ" },
{ "label": "__i", "body": "ᵢ", "description": "ᵢ" },
{ "label": "__k", "body": "ₖ", "description": "ₖ" },
{ "label": "__l", "body": "ₗ", "description": "ₗ" },
{ "label": "__m", "body": "ₘ", "description": "ₘ" },
{ "label": "__n", "body": "ₙ", "description": "ₙ" },
{ "label": "__o", "body": "ₒ", "description": "ₒ" },
{ "label": "__p", "body": "ₚ", "description": "ₚ" },
{ "label": "__r", "body": "ᵣ", "description": "ᵣ" },
{ "label": "__s", "body": "ₛ", "description": "ₛ" },
{ "label": "__t", "body": "ₜ", "description": "ₜ" },
{ "label": "__u", "body": "ᵤ", "description": "ᵤ" },
{ "label": "__v", "body": "ᵥ", "description": "ᵥ" },
{ "label": "__x", "body": "ₓ", "description": "ₓ" },
// Greek alphabet
{ "label": "Alpha", "body": "Α", "description": "Α" },
{ "label": "alpha", "body": "α", "description": "α" },
{ "label": "Beta", "body": "Β", "description": "Β" },
{ "label": "beta", "body": "β", "description": "β" },
{ "label": "Gamma", "body": "Γ", "description": "Γ" },
{ "label": "gamma", "body": "γ", "description": "γ" },
{ "label": "Delta", "body": "Δ", "description": "Δ" },
{ "label": "delta", "body": "δ", "description": "δ" },
{ "label": "Epsilon", "body": "Ε", "description": "Ε" },
{ "label": "epsilon", "body": "ε", "description": "ε" },
{ "label": "Zeta", "body": "Ζ", "description": "Ζ" },
{ "label": "zeta", "body": "ζ", "description": "ζ" },
{ "label": "Eta", "body": "Η", "description": "Η" },
{ "label": "eta", "body": "η", "description": "η" },
{ "label": "Theta", "body": "Θ", "description": "Θ" },
{ "label": "theta", "body": "θ", "description": "θ" },
{ "label": "Iota", "body": "Ι", "description": "Ι" },
{ "label": "iota", "body": "ι", "description": "ι" },
{ "label": "Kappa", "body": "Κ", "description": "Κ" },
{ "label": "kappa", "body": "κ", "description": "κ" },
{ "label": "Lamda", "body": "Λ", "description": "Λ" },
{ "label": "lamda", "body": "λ", "description": "λ" },
{ "label": "Lambda", "body": "Λ", "description": "Λ" },
{ "label": "lambda", "body": "λ", "description": "λ" },
{ "label": "Mu", "body": "Μ", "description": "Μ" },
{ "label": "mu", "body": "μ", "description": "μ" },
{ "label": "Nu", "body": "Ν", "description": "Ν" },
{ "label": "nu", "body": "ν", "description": "ν" },
{ "label": "Xi", "body": "Ξ", "description": "Ξ" },
{ "label": "xi", "body": "ξ", "description": "ξ" },
{ "label": "Omicron", "body": "Ο", "description": "Ο" },
{ "label": "omicron", "body": "ο", "description": "ο" },
{ "label": "Pi", "body": "Π", "description": "Π" },
{ "label": "pi", "body": "π", "description": "π" },
{ "label": "Rho", "body": "Ρ", "description": "Ρ" },
{ "label": "rho", "body": "ρ", "description": "ρ" },
{ "label": "Sigma", "body": "Σ", "description": "Σ" },
{ "label": "sigma", "body": "σ", "description": "σ" },
{ "label": "Tau", "body": "Τ", "description": "Τ" },
{ "label": "tau", "body": "τ", "description": "τ" },
{ "label": "Upsilon", "body": "Υ", "description": "Υ" },
{ "label": "upsilon", "body": "υ", "description": "υ" },
{ "label": "Phi", "body": "Φ", "description": "Φ" },
{ "label": "phi", "body": "φ", "description": "φ" },
{ "label": "Chi", "body": "Χ", "description": "Χ" },
{ "label": "chi", "body": "χ", "description": "χ" },
{ "label": "Psi", "body": "Ψ", "description": "Ψ" },
{ "label": "psi", "body": "ψ", "description": "ψ" },
{ "label": "Omega", "body": "Ω", "description": "Ω" },
{ "label": "omega", "body": "ω", "description": "ω" }
]
}
]
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment