From 57314d18609cb7a0949c9b80f457ff22a7fdfac0 Mon Sep 17 00:00:00 2001 From: Silvus Date: Mon, 22 Aug 2022 18:58:55 +0200 Subject: [PATCH 1/4] Added UltiSnips as an alternative way of inserting unicode characters in Vim --- docs/editor.md | 537 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 537 insertions(+) diff --git a/docs/editor.md b/docs/editor.md index 5ba7e03da..cd9b19684 100644 --- a/docs/editor.md +++ b/docs/editor.md @@ -688,3 +688,540 @@ let g:unicode_map = { \ "_x" : "ₓ", \ } ``` + + +Alternatively, you can use snippets using [UltiSnips](https://github.com/SirVer/ultisnips). + +Install it with your favorite plugin manager, and register a completion key in your configuration: +``` +let g:UltiSnipsExpandTrigger="" +``` +To insert a unicode character, type its trigger word, such as `\forall`, and then press `` while still in insert mode. + +To register most common unicode characters, put the following file either at `~/.vim/UltiSnips/coq_latex.snippets` or `~/.config/nvim/UltiSnips/coq_latex.snippets`, depending on your preferred variant of Vim: +``` +snippet \forall "" i +∀ +endsnippet +snippet \exists "" i +∃ +endsnippet +snippet \lam "" i +λ +endsnippet +snippet \not "" i +¬ +endsnippet +snippet \lor "" i +∨ +endsnippet +snippet \land "" i +∧ +endsnippet +snippet \/ "" i +∨ +endsnippet +snippet /\ "" i +∧ +endsnippet +snippet \rightarrow "" i +→ +endsnippet +snippet \implies "" i +→ +endsnippet +snippet -> "" i +→ +endsnippet +snippet \iff "" i +↔ +endsnippet +snippet <-> "" i +↔ +endsnippet +snippet \<- "" i +← +endsnippet +snippet \cong "" i +≡ +endsnippet +snippet \== "" i +≡ +endsnippet +snippet \/== "" i +≢ +endsnippet +snippet \neq "" i +≠ +endsnippet +snippet /= "" i +≠ +endsnippet +snippet \less "" i +≤ +endsnippet +snippet \le "" i +≤ +endsnippet +snippet <= "" i +≤ +endsnippet +snippet \in "" i +∈ +endsnippet +snippet \notin "" i +∉ +endsnippet +snippet \cup "" i +∪ +endsnippet +snippet \cap "" i +∩ +endsnippet +snippet \setminus "" i +∖ +endsnippet +snippet \subset "" i +⊂ +endsnippet +snippet \subseteq "" i +⊆ +endsnippet +snippet \sqsubseteq "" i +⊑ +endsnippet +snippet \sqsubseteq "" i +⊑ +endsnippet +snippet \notsubseteq "" i +⊈ +endsnippet +snippet \meet "" i +⊓ +endsnippet +snippet \join "" i +⊔ +endsnippet +snippet \true "" i +⊤ +endsnippet +snippet \top "" i +⊤ +endsnippet +snippet \false "" i +⊥ +endsnippet +snippet \bottom "" i +⊥ +endsnippet +snippet \vdash "" i +⊢ +endsnippet +snippet \dashv "" i +⊣ +endsnippet +snippet \vDash "" i +⊨ +endsnippet +snippet \Vdash +⊩ +endsnippet +snippet \infty "" i +∞ +endsnippet +snippet \comp "" i +∘ +endsnippet +snippet \prf "" i +↾ +endsnippet +snippet \bind "" i +≫= +endsnippet +snippet \mapsto "" i +↦ +endsnippet +snippet \hookrightarrow "" i +↪ +endsnippet +snippet \up "" i +↑ +endsnippet +snippet \uparrow "" i +↑ +endsnippet + +snippet \fun "" i +λ +endsnippet +snippet \mult "" i +⋅ +endsnippet +snippet \ent "" i +⊢ +endsnippet +snippet \valid "" i +✓ +endsnippet +snippet \diamond "" i +◇ +endsnippet +snippet \box "" i +□ +endsnippet +snippet \bbox "" i +■ +endsnippet +snippet \eval "" i +▷ +endsnippet +snippet \rhd "" i +▷ +endsnippet +snippet \later "" i +▷ +endsnippet +snippet \pred "" i +φ +endsnippet +snippet \and "" i +∧ +endsnippet +snippet \or "" i +∨ +endsnippet +snippet \circ "" i +∘ +endsnippet +snippet \comp "" i +∘ +endsnippet +snippet \ccomp "" i +◎ +endsnippet +snippet \pound "" i +£ +endsnippet +snippet \all "" i +∀ +endsnippet +snippet \ex "" i +∃ +endsnippet +snippet \to "" i +→ +endsnippet +snippet \ast "" i +∗ +endsnippet +snippet \sep "" i +∗ +endsnippet +snippet \ulc "" i +⌜ +endsnippet +snippet \urc "" i +⌝ +endsnippet +snippet \lc "" i +⌜ +endsnippet +snippet \rc "" i +⌝ +endsnippet +snippet \Lc "" i +⎡ +endsnippet +snippet \Rc "" i +⎤ +endsnippet +snippet \varnothing "" i +∅ +endsnippet +snippet \empty "" i +∅ +endsnippet +snippet \Lam "" i +Λ +endsnippet +snippet \Sig "" i +Σ +endsnippet +snippet \- "" i +∖ +endsnippet +snippet \aa "" i +● +endsnippet +snippet \af "" i +◯ +endsnippet +snippet \auth "" i +● +endsnippet +snippet \frag "" i +◯ +endsnippet +snippet \iff "" i +↔ +endsnippet +snippet \gname "" i +γ +endsnippet +snippet \incl "" i +≼ +endsnippet +snippet \latert "" i +▶ +endsnippet +snippet \update "" i +⇝ +endsnippet +snippet \bind "" i +≫= +endsnippet + + +snippet ^^+ "" i +⁺ +endsnippet +snippet __+ "" i +₊ +endsnippet +snippet ^^- "" i +⁻ +endsnippet +snippet __0 "" i +₀ +endsnippet +snippet __1 "" i +₁ +endsnippet +snippet __2 "" i +₂ +endsnippet +snippet __3 "" i +₃ +endsnippet +snippet __4 "" i +₄ +endsnippet +snippet __5 "" i +₅ +endsnippet +snippet __6 "" i +₆ +endsnippet +snippet __7 "" i +₇ +endsnippet +snippet __8 "" i +₈ +endsnippet +snippet __9 "" i +₉ +endsnippet + +snippet __a "" i +ₐ +endsnippet +snippet __e "" i +ₑ +endsnippet +snippet __h "" i +ₕ +endsnippet +snippet __i "" i +ᵢ +endsnippet +snippet __k "" i +ₖ +endsnippet +snippet __l "" i +ₗ +endsnippet +snippet __m "" i +ₘ +endsnippet +snippet __n "" i +ₙ +endsnippet +snippet __o "" i +ₒ +endsnippet +snippet __p "" i +ₚ +endsnippet +snippet __r "" i +ᵣ +endsnippet +snippet __s "" i +ₛ +endsnippet +snippet __t "" i +ₜ +endsnippet +snippet __u "" i +ᵤ +endsnippet +snippet __v "" i +ᵥ +endsnippet +snippet __x "" i +ₓ +endsnippet + +snippet \Alpha "" i +Α +endsnippet +snippet \alpha "" i +α +endsnippet +snippet \Beta "" i +Β +endsnippet +snippet \beta "" i +β +endsnippet +snippet \Gamma "" i +Γ +endsnippet +snippet \gamma "" i +γ +endsnippet +snippet \Delta "" i +Δ +endsnippet +snippet \delta "" i +δ +endsnippet +snippet \Epsilon "" i +Ε +endsnippet +snippet \epsilon "" i +ε +endsnippet +snippet \Zeta "" i +Ζ +endsnippet +snippet \zeta "" i +ζ +endsnippet +snippet \Eta "" i +Η +endsnippet +snippet \eta "" i +η +endsnippet +snippet \Theta "" i +Θ +endsnippet +snippet \theta "" i +θ +endsnippet +snippet \Iota "" i +Ι +endsnippet +snippet \iota "" i +ι +endsnippet +snippet \Kappa "" i +Κ +endsnippet +snippet \kappa "" i +κ +endsnippet +snippet \Lamda "" i +Λ +endsnippet +snippet \lamda "" i +λ +endsnippet +snippet \Lambda "" i +Λ +endsnippet +snippet \lambda "" i +λ +endsnippet +snippet \Mu "" i +Μ +endsnippet +snippet \mu "" i +μ +endsnippet +snippet \Nu "" i +Ν +endsnippet +snippet \nu "" i +ν +endsnippet +snippet \Xi "" i +Ξ +endsnippet +snippet \xi "" i +ξ +endsnippet +snippet \Omicron "" i +Ο +endsnippet +snippet \omicron "" i +ο +endsnippet +snippet \Pi "" i +Π +endsnippet +snippet \pi "" i +π +endsnippet +snippet \Rho "" i +Ρ +endsnippet +snippet \rho "" i +ρ +endsnippet +snippet \Sigma "" i +Σ +endsnippet +snippet \sigma "" i +σ +endsnippet +snippet \Tau "" i +Τ +endsnippet +snippet \tau "" i +τ +endsnippet +snippet \Upsilon "" i +Υ +endsnippet +snippet \upsilon "" i +υ +endsnippet +snippet \Phi "" i +Φ +endsnippet +snippet \phi "" i +ϕ +endsnippet +snippet \varphi "" i +φ +endsnippet +snippet \Chi "" i +Χ +endsnippet +snippet \chi "" i +χ +endsnippet +snippet \Psi "" i +Ψ +endsnippet +snippet \psi "" i +ψ +endsnippet +snippet \Omega "" i +Ω +endsnippet +snippet \omega "" i +ω +endsnippet +``` -- GitLab From ae2251fc7721a6c985351db06dbb0f66171c705f Mon Sep 17 00:00:00 2001 From: Silvus Date: Thu, 25 Aug 2022 08:54:46 +0200 Subject: [PATCH 2/4] Fixed ilnk to iris/bi/ascii.v --- docs/editor.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/editor.md b/docs/editor.md index cd9b19684..92ff9a3ee 100644 --- a/docs/editor.md +++ b/docs/editor.md @@ -5,7 +5,7 @@ If you really want to, you can also avoid having to type unicode characters by importing `iris.bi.ascii`. That enables parsing-only ASCII alternatives to many unicode notations. (Feel free to report an issue when you notice that a notation is missing.) The easiest way to learn the ASCII syntax is to -[read this file](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/theories/bi/ascii.v). +[read this file](/iris/bi/ascii.v). Note however that this will make your code harder to read and work on for Iris developers that are used to our default unicode notation---generally, our recommendation is to use the unicode syntax whenever possible. In particular, -- GitLab From 0f8cd146e6d995e254e76545f396561849035e9c Mon Sep 17 00:00:00 2001 From: Silvus Date: Thu, 25 Aug 2022 08:56:13 +0200 Subject: [PATCH 3/4] moved ultisnips configuration to its own file --- docs/coq_latex.snippets | 524 +++++++++++++++++++++++++++++++++++++++ docs/editor.md | 530 +--------------------------------------- 2 files changed, 526 insertions(+), 528 deletions(-) create mode 100644 docs/coq_latex.snippets diff --git a/docs/coq_latex.snippets b/docs/coq_latex.snippets new file mode 100644 index 000000000..758b3a99e --- /dev/null +++ b/docs/coq_latex.snippets @@ -0,0 +1,524 @@ +snippet \forall "" i +∀ +endsnippet +snippet \exists "" i +∃ +endsnippet +snippet \lam "" i +λ +endsnippet +snippet \not "" i +¬ +endsnippet +snippet \lor "" i +∨ +endsnippet +snippet \land "" i +∧ +endsnippet +snippet \/ "" i +∨ +endsnippet +snippet /\ "" i +∧ +endsnippet +snippet \rightarrow "" i +→ +endsnippet +snippet \implies "" i +→ +endsnippet +snippet -> "" i +→ +endsnippet +snippet \iff "" i +↔ +endsnippet +snippet <-> "" i +↔ +endsnippet +snippet \<- "" i +← +endsnippet +snippet \cong "" i +≡ +endsnippet +snippet \== "" i +≡ +endsnippet +snippet \/== "" i +≢ +endsnippet +snippet \neq "" i +≠ +endsnippet +snippet /= "" i +≠ +endsnippet +snippet \less "" i +≤ +endsnippet +snippet \le "" i +≤ +endsnippet +snippet <= "" i +≤ +endsnippet +snippet \in "" i +∈ +endsnippet +snippet \notin "" i +∉ +endsnippet +snippet \cup "" i +∪ +endsnippet +snippet \cap "" i +∩ +endsnippet +snippet \setminus "" i +∖ +endsnippet +snippet \subset "" i +⊂ +endsnippet +snippet \subseteq "" i +⊆ +endsnippet +snippet \sqsubseteq "" i +⊑ +endsnippet +snippet \sqsubseteq "" i +⊑ +endsnippet +snippet \notsubseteq "" i +⊈ +endsnippet +snippet \meet "" i +⊓ +endsnippet +snippet \join "" i +⊔ +endsnippet +snippet \true "" i +⊤ +endsnippet +snippet \top "" i +⊤ +endsnippet +snippet \false "" i +⊥ +endsnippet +snippet \bottom "" i +⊥ +endsnippet +snippet \vdash "" i +⊢ +endsnippet +snippet \dashv "" i +⊣ +endsnippet +snippet \vDash "" i +⊨ +endsnippet +snippet \Vdash +⊩ +endsnippet +snippet \infty "" i +∞ +endsnippet +snippet \comp "" i +∘ +endsnippet +snippet \prf "" i +↾ +endsnippet +snippet \bind "" i +≫= +endsnippet +snippet \mapsto "" i +↦ +endsnippet +snippet \hookrightarrow "" i +↪ +endsnippet +snippet \up "" i +↑ +endsnippet +snippet \uparrow "" i +↑ +endsnippet + +snippet \fun "" i +λ +endsnippet +snippet \mult "" i +⋅ +endsnippet +snippet \ent "" i +⊢ +endsnippet +snippet \valid "" i +✓ +endsnippet +snippet \diamond "" i +◇ +endsnippet +snippet \box "" i +□ +endsnippet +snippet \bbox "" i +■ +endsnippet +snippet \eval "" i +▷ +endsnippet +snippet \rhd "" i +▷ +endsnippet +snippet \later "" i +▷ +endsnippet +snippet \pred "" i +φ +endsnippet +snippet \and "" i +∧ +endsnippet +snippet \or "" i +∨ +endsnippet +snippet \circ "" i +∘ +endsnippet +snippet \comp "" i +∘ +endsnippet +snippet \ccomp "" i +◎ +endsnippet +snippet \pound "" i +£ +endsnippet +snippet \all "" i +∀ +endsnippet +snippet \ex "" i +∃ +endsnippet +snippet \to "" i +→ +endsnippet +snippet \ast "" i +∗ +endsnippet +snippet \sep "" i +∗ +endsnippet +snippet \ulc "" i +⌜ +endsnippet +snippet \urc "" i +⌝ +endsnippet +snippet \lc "" i +⌜ +endsnippet +snippet \rc "" i +⌝ +endsnippet +snippet \Lc "" i +⎡ +endsnippet +snippet \Rc "" i +⎤ +endsnippet +snippet \varnothing "" i +∅ +endsnippet +snippet \empty "" i +∅ +endsnippet +snippet \Lam "" i +Λ +endsnippet +snippet \Sig "" i +Σ +endsnippet +snippet \- "" i +∖ +endsnippet +snippet \aa "" i +● +endsnippet +snippet \af "" i +◯ +endsnippet +snippet \auth "" i +● +endsnippet +snippet \frag "" i +◯ +endsnippet +snippet \iff "" i +↔ +endsnippet +snippet \gname "" i +γ +endsnippet +snippet \incl "" i +≼ +endsnippet +snippet \latert "" i +▶ +endsnippet +snippet \update "" i +⇝ +endsnippet +snippet \bind "" i +≫= +endsnippet + + +snippet ^^+ "" i +⁺ +endsnippet +snippet __+ "" i +₊ +endsnippet +snippet ^^- "" i +⁻ +endsnippet +snippet __0 "" i +₀ +endsnippet +snippet __1 "" i +₁ +endsnippet +snippet __2 "" i +₂ +endsnippet +snippet __3 "" i +₃ +endsnippet +snippet __4 "" i +₄ +endsnippet +snippet __5 "" i +₅ +endsnippet +snippet __6 "" i +₆ +endsnippet +snippet __7 "" i +₇ +endsnippet +snippet __8 "" i +₈ +endsnippet +snippet __9 "" i +₉ +endsnippet + +snippet __a "" i +ₐ +endsnippet +snippet __e "" i +ₑ +endsnippet +snippet __h "" i +ₕ +endsnippet +snippet __i "" i +ᵢ +endsnippet +snippet __k "" i +ₖ +endsnippet +snippet __l "" i +ₗ +endsnippet +snippet __m "" i +ₘ +endsnippet +snippet __n "" i +ₙ +endsnippet +snippet __o "" i +ₒ +endsnippet +snippet __p "" i +ₚ +endsnippet +snippet __r "" i +ᵣ +endsnippet +snippet __s "" i +ₛ +endsnippet +snippet __t "" i +ₜ +endsnippet +snippet __u "" i +ᵤ +endsnippet +snippet __v "" i +ᵥ +endsnippet +snippet __x "" i +ₓ +endsnippet + +snippet \Alpha "" i +Α +endsnippet +snippet \alpha "" i +α +endsnippet +snippet \Beta "" i +Β +endsnippet +snippet \beta "" i +β +endsnippet +snippet \Gamma "" i +Γ +endsnippet +snippet \gamma "" i +γ +endsnippet +snippet \Delta "" i +Δ +endsnippet +snippet \delta "" i +δ +endsnippet +snippet \Epsilon "" i +Ε +endsnippet +snippet \epsilon "" i +ε +endsnippet +snippet \Zeta "" i +Ζ +endsnippet +snippet \zeta "" i +ζ +endsnippet +snippet \Eta "" i +Η +endsnippet +snippet \eta "" i +η +endsnippet +snippet \Theta "" i +Θ +endsnippet +snippet \theta "" i +θ +endsnippet +snippet \Iota "" i +Ι +endsnippet +snippet \iota "" i +ι +endsnippet +snippet \Kappa "" i +Κ +endsnippet +snippet \kappa "" i +κ +endsnippet +snippet \Lamda "" i +Λ +endsnippet +snippet \lamda "" i +λ +endsnippet +snippet \Lambda "" i +Λ +endsnippet +snippet \lambda "" i +λ +endsnippet +snippet \Mu "" i +Μ +endsnippet +snippet \mu "" i +μ +endsnippet +snippet \Nu "" i +Ν +endsnippet +snippet \nu "" i +ν +endsnippet +snippet \Xi "" i +Ξ +endsnippet +snippet \xi "" i +ξ +endsnippet +snippet \Omicron "" i +Ο +endsnippet +snippet \omicron "" i +ο +endsnippet +snippet \Pi "" i +Π +endsnippet +snippet \pi "" i +π +endsnippet +snippet \Rho "" i +Ρ +endsnippet +snippet \rho "" i +ρ +endsnippet +snippet \Sigma "" i +Σ +endsnippet +snippet \sigma "" i +σ +endsnippet +snippet \Tau "" i +Τ +endsnippet +snippet \tau "" i +τ +endsnippet +snippet \Upsilon "" i +Υ +endsnippet +snippet \upsilon "" i +υ +endsnippet +snippet \Phi "" i +Φ +endsnippet +snippet \phi "" i +ϕ +endsnippet +snippet \varphi "" i +φ +endsnippet +snippet \Chi "" i +Χ +endsnippet +snippet \chi "" i +χ +endsnippet +snippet \Psi "" i +Ψ +endsnippet +snippet \psi "" i +ψ +endsnippet +snippet \Omega "" i +Ω +endsnippet +snippet \omega "" i +ω +endsnippet diff --git a/docs/editor.md b/docs/editor.md index 92ff9a3ee..b4f8ac2d8 100644 --- a/docs/editor.md +++ b/docs/editor.md @@ -696,532 +696,6 @@ Install it with your favorite plugin manager, and register a completion key in y ``` let g:UltiSnipsExpandTrigger="" ``` -To insert a unicode character, type its trigger word, such as `\forall`, and then press `` while still in insert mode. +To insert a unicode character, type its trigger word, such as `\forall` or `->`, and then press `` while still in insert mode. -To register most common unicode characters, put the following file either at `~/.vim/UltiSnips/coq_latex.snippets` or `~/.config/nvim/UltiSnips/coq_latex.snippets`, depending on your preferred variant of Vim: -``` -snippet \forall "" i -∀ -endsnippet -snippet \exists "" i -∃ -endsnippet -snippet \lam "" i -λ -endsnippet -snippet \not "" i -¬ -endsnippet -snippet \lor "" i -∨ -endsnippet -snippet \land "" i -∧ -endsnippet -snippet \/ "" i -∨ -endsnippet -snippet /\ "" i -∧ -endsnippet -snippet \rightarrow "" i -→ -endsnippet -snippet \implies "" i -→ -endsnippet -snippet -> "" i -→ -endsnippet -snippet \iff "" i -↔ -endsnippet -snippet <-> "" i -↔ -endsnippet -snippet \<- "" i -← -endsnippet -snippet \cong "" i -≡ -endsnippet -snippet \== "" i -≡ -endsnippet -snippet \/== "" i -≢ -endsnippet -snippet \neq "" i -≠ -endsnippet -snippet /= "" i -≠ -endsnippet -snippet \less "" i -≤ -endsnippet -snippet \le "" i -≤ -endsnippet -snippet <= "" i -≤ -endsnippet -snippet \in "" i -∈ -endsnippet -snippet \notin "" i -∉ -endsnippet -snippet \cup "" i -∪ -endsnippet -snippet \cap "" i -∩ -endsnippet -snippet \setminus "" i -∖ -endsnippet -snippet \subset "" i -⊂ -endsnippet -snippet \subseteq "" i -⊆ -endsnippet -snippet \sqsubseteq "" i -⊑ -endsnippet -snippet \sqsubseteq "" i -⊑ -endsnippet -snippet \notsubseteq "" i -⊈ -endsnippet -snippet \meet "" i -⊓ -endsnippet -snippet \join "" i -⊔ -endsnippet -snippet \true "" i -⊤ -endsnippet -snippet \top "" i -⊤ -endsnippet -snippet \false "" i -⊥ -endsnippet -snippet \bottom "" i -⊥ -endsnippet -snippet \vdash "" i -⊢ -endsnippet -snippet \dashv "" i -⊣ -endsnippet -snippet \vDash "" i -⊨ -endsnippet -snippet \Vdash -⊩ -endsnippet -snippet \infty "" i -∞ -endsnippet -snippet \comp "" i -∘ -endsnippet -snippet \prf "" i -↾ -endsnippet -snippet \bind "" i -≫= -endsnippet -snippet \mapsto "" i -↦ -endsnippet -snippet \hookrightarrow "" i -↪ -endsnippet -snippet \up "" i -↑ -endsnippet -snippet \uparrow "" i -↑ -endsnippet - -snippet \fun "" i -λ -endsnippet -snippet \mult "" i -⋅ -endsnippet -snippet \ent "" i -⊢ -endsnippet -snippet \valid "" i -✓ -endsnippet -snippet \diamond "" i -◇ -endsnippet -snippet \box "" i -□ -endsnippet -snippet \bbox "" i -■ -endsnippet -snippet \eval "" i -▷ -endsnippet -snippet \rhd "" i -▷ -endsnippet -snippet \later "" i -▷ -endsnippet -snippet \pred "" i -φ -endsnippet -snippet \and "" i -∧ -endsnippet -snippet \or "" i -∨ -endsnippet -snippet \circ "" i -∘ -endsnippet -snippet \comp "" i -∘ -endsnippet -snippet \ccomp "" i -◎ -endsnippet -snippet \pound "" i -£ -endsnippet -snippet \all "" i -∀ -endsnippet -snippet \ex "" i -∃ -endsnippet -snippet \to "" i -→ -endsnippet -snippet \ast "" i -∗ -endsnippet -snippet \sep "" i -∗ -endsnippet -snippet \ulc "" i -⌜ -endsnippet -snippet \urc "" i -⌝ -endsnippet -snippet \lc "" i -⌜ -endsnippet -snippet \rc "" i -⌝ -endsnippet -snippet \Lc "" i -⎡ -endsnippet -snippet \Rc "" i -⎤ -endsnippet -snippet \varnothing "" i -∅ -endsnippet -snippet \empty "" i -∅ -endsnippet -snippet \Lam "" i -Λ -endsnippet -snippet \Sig "" i -Σ -endsnippet -snippet \- "" i -∖ -endsnippet -snippet \aa "" i -● -endsnippet -snippet \af "" i -◯ -endsnippet -snippet \auth "" i -● -endsnippet -snippet \frag "" i -◯ -endsnippet -snippet \iff "" i -↔ -endsnippet -snippet \gname "" i -γ -endsnippet -snippet \incl "" i -≼ -endsnippet -snippet \latert "" i -▶ -endsnippet -snippet \update "" i -⇝ -endsnippet -snippet \bind "" i -≫= -endsnippet - - -snippet ^^+ "" i -⁺ -endsnippet -snippet __+ "" i -₊ -endsnippet -snippet ^^- "" i -⁻ -endsnippet -snippet __0 "" i -₀ -endsnippet -snippet __1 "" i -₁ -endsnippet -snippet __2 "" i -₂ -endsnippet -snippet __3 "" i -₃ -endsnippet -snippet __4 "" i -₄ -endsnippet -snippet __5 "" i -₅ -endsnippet -snippet __6 "" i -₆ -endsnippet -snippet __7 "" i -₇ -endsnippet -snippet __8 "" i -₈ -endsnippet -snippet __9 "" i -₉ -endsnippet - -snippet __a "" i -ₐ -endsnippet -snippet __e "" i -ₑ -endsnippet -snippet __h "" i -ₕ -endsnippet -snippet __i "" i -ᵢ -endsnippet -snippet __k "" i -ₖ -endsnippet -snippet __l "" i -ₗ -endsnippet -snippet __m "" i -ₘ -endsnippet -snippet __n "" i -ₙ -endsnippet -snippet __o "" i -ₒ -endsnippet -snippet __p "" i -ₚ -endsnippet -snippet __r "" i -ᵣ -endsnippet -snippet __s "" i -ₛ -endsnippet -snippet __t "" i -ₜ -endsnippet -snippet __u "" i -ᵤ -endsnippet -snippet __v "" i -ᵥ -endsnippet -snippet __x "" i -ₓ -endsnippet - -snippet \Alpha "" i -Α -endsnippet -snippet \alpha "" i -α -endsnippet -snippet \Beta "" i -Β -endsnippet -snippet \beta "" i -β -endsnippet -snippet \Gamma "" i -Γ -endsnippet -snippet \gamma "" i -γ -endsnippet -snippet \Delta "" i -Δ -endsnippet -snippet \delta "" i -δ -endsnippet -snippet \Epsilon "" i -Ε -endsnippet -snippet \epsilon "" i -ε -endsnippet -snippet \Zeta "" i -Ζ -endsnippet -snippet \zeta "" i -ζ -endsnippet -snippet \Eta "" i -Η -endsnippet -snippet \eta "" i -η -endsnippet -snippet \Theta "" i -Θ -endsnippet -snippet \theta "" i -θ -endsnippet -snippet \Iota "" i -Ι -endsnippet -snippet \iota "" i -ι -endsnippet -snippet \Kappa "" i -Κ -endsnippet -snippet \kappa "" i -κ -endsnippet -snippet \Lamda "" i -Λ -endsnippet -snippet \lamda "" i -λ -endsnippet -snippet \Lambda "" i -Λ -endsnippet -snippet \lambda "" i -λ -endsnippet -snippet \Mu "" i -Μ -endsnippet -snippet \mu "" i -μ -endsnippet -snippet \Nu "" i -Ν -endsnippet -snippet \nu "" i -ν -endsnippet -snippet \Xi "" i -Ξ -endsnippet -snippet \xi "" i -ξ -endsnippet -snippet \Omicron "" i -Ο -endsnippet -snippet \omicron "" i -ο -endsnippet -snippet \Pi "" i -Π -endsnippet -snippet \pi "" i -π -endsnippet -snippet \Rho "" i -Ρ -endsnippet -snippet \rho "" i -ρ -endsnippet -snippet \Sigma "" i -Σ -endsnippet -snippet \sigma "" i -σ -endsnippet -snippet \Tau "" i -Τ -endsnippet -snippet \tau "" i -τ -endsnippet -snippet \Upsilon "" i -Υ -endsnippet -snippet \upsilon "" i -υ -endsnippet -snippet \Phi "" i -Φ -endsnippet -snippet \phi "" i -ϕ -endsnippet -snippet \varphi "" i -φ -endsnippet -snippet \Chi "" i -Χ -endsnippet -snippet \chi "" i -χ -endsnippet -snippet \Psi "" i -Ψ -endsnippet -snippet \psi "" i -ψ -endsnippet -snippet \Omega "" i -Ω -endsnippet -snippet \omega "" i -ω -endsnippet -``` +To register most common unicode characters, put [this file](/docs/coq_latex.snippets) either at `~/.vim/UltiSnips/coq_latex.snippets` or `~/.config/nvim/UltiSnips/coq_latex.snippets`, depending on your preferred variant of Vim. -- GitLab From 2cdead8744b5e45f1c71bb7bb1bfd91d8b23d6b5 Mon Sep 17 00:00:00 2001 From: Silvus Date: Fri, 26 Aug 2022 19:00:25 +0200 Subject: [PATCH 4/4] renamed configuration file --- docs/editor.md | 2 +- docs/{coq_latex.snippets => vim_ultisnips} | 0 2 files changed, 1 insertion(+), 1 deletion(-) rename docs/{coq_latex.snippets => vim_ultisnips} (100%) diff --git a/docs/editor.md b/docs/editor.md index b4f8ac2d8..993997cbb 100644 --- a/docs/editor.md +++ b/docs/editor.md @@ -698,4 +698,4 @@ let g:UltiSnipsExpandTrigger="" ``` To insert a unicode character, type its trigger word, such as `\forall` or `->`, and then press `` while still in insert mode. -To register most common unicode characters, put [this file](/docs/coq_latex.snippets) either at `~/.vim/UltiSnips/coq_latex.snippets` or `~/.config/nvim/UltiSnips/coq_latex.snippets`, depending on your preferred variant of Vim. +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. diff --git a/docs/coq_latex.snippets b/docs/vim_ultisnips similarity index 100% rename from docs/coq_latex.snippets rename to docs/vim_ultisnips -- GitLab