From 778e70edc5865766f792ddc8e5079cf1ad1ab606 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Fri, 15 Oct 2021 23:02:49 +0200
Subject: [PATCH] vim editor docs

---
 docs/editor.md | 71 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 71 insertions(+)

diff --git a/docs/editor.md b/docs/editor.md
index e2a052efc..438252da9 100644
--- a/docs/editor.md
+++ b/docs/editor.md
@@ -565,3 +565,74 @@ click on "Edit in settings.json" and add the following:
         }
     ]
 ```
+
+
+## Vim
+
+The [Coqtail](https://github.com/whonore/coqtail) plugin can be used to develop Coq code in `vim` (install it with your favorite plugin manager).
+Follow the installation instructions in Coqtail's README to setup your keybinds and find out about its usage.
+
+### Unicode support
+For Unicode support, make sure that your terminal emulator supports Unicode and configure it to use a font with Unicode support.
+
+For entering Unicode symbols, one option is the plugin [latex-unicoder](https://github.com/joom/latex-unicoder.vim).
+Install it with your favorite plugin manager.
+To enter a Unicode symbol, hit `C-l` in normal or insert mode. For more details on the usage, see its README.
+
+latex-unicoder comes with a large set of pre-configured symbols known from LaTeX, but you can also add your own by adding (and adapting) the following to your `.vimrc`:
+```
+let g:unicode_map = {
+  \ "\\fun"     :   "λ",
+  \ "\\mult"    :   "â‹…",
+  \ "\\ent"     :   "⊢",
+  \ "\\valid"   :   "✓",
+  \ "\\diamond" :   "â—‡",
+  \ "\\box"     :   "â–¡",
+  \ "\\bbox"   	:   "â– ",
+  \ "\\later"  	:   "â–·",
+  \ "\\pred"   	:   "φ",
+  \ "\\and"    	:   "∧",
+  \ "\\or"     	:   "∨",
+  \ "\\comp"   	:   "∘",
+  \ "\\ccomp"  	:   "â—Ž",
+  \ "\\all"    	:   "∀",
+  \ "\\ex"     	:   "∃",
+  \ "\\to"     	:   "→",
+  \ "\\sep"    	:   "∗",
+  \ "\\lc"     	:   "⌜",
+  \ "\\rc"     	:   "⌝",
+  \ "\\Lc"     	:   "⎡",
+  \ "\\Rc"     	:   "⎤",
+  \ "\\lam"    	:   "λ",
+  \ "\\empty"  	:   "∅",
+  \ "\\Lam"    	:   "Λ",
+  \ "\\Sig"    	:   "Σ",
+  \ "\\-"      	:   "∖",
+  \ "\\aa"     	:   "●",
+  \ "\\af"     	:   "â—¯",
+  \ "\\auth"   	:   "●",
+  \ "\\frag"   	:   "â—¯",
+  \ "\\iff"    	:   "↔",
+  \ "\\gname"  	:   "γ",
+  \ "\\incl"   	:   "≼",
+  \ "\\latert" 	:   "â–¶",
+  \ "\\update" 	:   "⇝",
+  \ "\\\"o"     :   "ö",
+  \ "_a"        :   "ₐ",
+  \ "_e"        :   "â‚‘",
+  \ "_h"        :   "â‚•",
+  \ "_i"        :   "áµ¢",
+  \ "_k"        :   "â‚–",
+  \ "_l"        :   "â‚—",
+  \ "_m"        :   "ₘ",
+  \ "_n"        :   "â‚™",
+  \ "_o"        :   "â‚’",
+  \ "_p"        :   "â‚š",
+  \ "_r"        :   "áµ£",
+  \ "_s"        :   "â‚›",
+  \ "_t"        :   "ₜ",
+  \ "_u"        :   "ᵤ",
+  \ "_v"        :   "áµ¥",
+  \ "_x"        :   "â‚“",
+\ }
+```
-- 
GitLab