diff --git a/docs/editor.md b/docs/editor.md
index 993997cbb2450181ca3b9eb738d97a2cdb4dd5cb..115b1fc3721d100309f586247f822adcd4384464 100644
--- a/docs/editor.md
+++ b/docs/editor.md
@@ -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.
diff --git a/docs/ibus b/docs/ibus
new file mode 100644
index 0000000000000000000000000000000000000000..18dde673f1745f967fc5e17110f1705f94e794be
--- /dev/null
+++ b/docs/ibus
@@ -0,0 +1,124 @@
+;; 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)))
diff --git a/docs/vscode b/docs/vscode
new file mode 100644
index 0000000000000000000000000000000000000000..9a77a165d299cc6bae9e7c7bab441f6b63240edf
--- /dev/null
+++ b/docs/vscode
@@ -0,0 +1,178 @@
+ "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": "ω" }
+ ]
+ }
+ ]