Latex Snippets - siegebell/vscoq GitHub Wiki

Auto-completion for common Unicode symbols using latex macros.

  1. Run "Preferences: Open User Snippets"
  2. Select "Coq" as the target language
  3. Paste the following between the curly braces:
"Alpha": { "prefix": "\\Alpha Ξ‘", "body": "Ξ‘", "description": "Alpha" },
"alpha": { "prefix": "\\alpha Ξ±", "body": "Ξ±", "description": "alpha" },
"Beta": { "prefix": "\\Beta Ξ’", "body": "Ξ’", "description": "Beta" },
"beta": { "prefix": "\\beta Ξ²", "body": "Ξ²", "description": "beta" },
"Gamma": { "prefix": "\\Gamma Ξ“", "body": "Ξ“", "description": "Gamma" },
"gamma": { "prefix": "\\gamma Ξ³", "body": "Ξ³", "description": "gamma" },
"Delta": { "prefix": "\\Delta Ξ”", "body": "Ξ”", "description": "Delta" },
"delta": { "prefix": "\\delta Ξ΄", "body": "Ξ΄", "description": "delta" },
"Epsilon": { "prefix": "\\Epsilon Ξ•", "body": "Ξ•", "description": "Epsilon" },
"epsilon": { "prefix": "\\epsilon Ξ΅", "body": "Ξ΅", "description": "epsilon" },
"varepsilon": { "prefix": "\\varepsilon Ξ΅", "body": "Ξ΅", "description": "varepsilon" },
"Zeta": { "prefix": "\\Zeta Ξ–", "body": "Ξ–", "description": "Zeta" },
"zeta": { "prefix": "\\zeta ΞΆ", "body": "ΞΆ", "description": "zeta" },
"Eta": { "prefix": "\\Eta Ξ—", "body": "Ξ—", "description": "Eta" },
"eta": { "prefix": "\\eta Ξ·", "body": "Ξ·", "description": "eta" },
"Theta": { "prefix": "\\Theta Θ", "body": "Θ", "description": "Theta" },
"theta": { "prefix": "\\theta ΞΈ", "body": "ΞΈ", "description": "theta" },
"vartheta": { "prefix": "\\vartheta Ο‘", "body": "Ο‘", "description": "vartheta" },
"Iota": { "prefix": "\\Iota Ξ™", "body": "Ξ™", "description": "Iota" },
"iota": { "prefix": "\\iota ΞΉ", "body": "ΞΉ", "description": "iota" },
"Kappa": { "prefix": "\\Kappa Κ", "body": "Κ", "description": "Kappa" },
"kappa": { "prefix": "\\kappa ΞΊ", "body": "ΞΊ", "description": "kappa" },
"varkappa": { "prefix": "\\varkappa ΞΊ", "body": "ΞΊ", "description": "varkappa" },
"Lambda": { "prefix": "\\Lambda Ξ›", "body": "Ξ›", "description": "Lambda" },
"lambda": { "prefix": "\\lambda Ξ»", "body": "Ξ»", "description": "lambda" },
"Mu": { "prefix": "\\Mu Μ", "body": "Μ", "description": "Mu" },
"mu": { "prefix": "\\mu ΞΌ", "body": "ΞΌ", "description": "mu" },
"Nu": { "prefix": "\\Nu Ν", "body": "Ν", "description": "Nu" },
"nu": { "prefix": "\\nu Ξ½", "body": "Ξ½", "description": "nu" },
"Xi": { "prefix": "\\Xi Ξ", "body": "Ξ", "description": "Xi" },
"xi": { "prefix": "\\xi ΞΎ", "body": "ΞΎ", "description": "xi" },
"Omicron": { "prefix": "\\Omicron Ο", "body": "Ο", "description": "Omicron" },
"omicron": { "prefix": "\\omicron ΞΏ", "body": "ΞΏ", "description": "omicron" },
"Pi": { "prefix": "\\Pi Ξ ", "body": "Ξ ", "description": "Pi" },
"pi": { "prefix": "\\pi Ο€", "body": "Ο€", "description": "pi" },
"Rho": { "prefix": "\\Rho Ξ‘", "body": "Ξ‘", "description": "Rho" },
"rho": { "prefix": "\\rho ρ", "body": "ρ", "description": "rho" },
"Sigma": { "prefix": "\\Sigma Ξ£", "body": "Ξ£", "description": "Sigma" },
"sigma": { "prefix": "\\sigma Οƒ", "body": "Οƒ", "description": "sigma" },
"varsigma": { "prefix": "\\varsigma Ο‚", "body": "Ο‚", "description": "varsigma" },
"Tau": { "prefix": "\\Tau Ξ€", "body": "Ξ€", "description": "Tau" },
"tau": { "prefix": "\\tau Ο„", "body": "Ο„", "description": "tau" },
"Upsilon": { "prefix": "\\Upsilon Ξ₯", "body": "Ξ₯", "description": "Upsilon" },
"upsilon": { "prefix": "\\upsilon Ο…", "body": "Ο…", "description": "upsilon" },
"Phi": { "prefix": "\\Phi Ξ¦", "body": "Ξ¦", "description": "Phi" },
"phi": { "prefix": "\\phi Ο†", "body": "Ο†", "description": "phi" },
"varphi": { "prefix": "\\varphi Ο•", "body": "Ο•", "description": "varphi" },
"Chi": { "prefix": "\\Chi Ξ§", "body": "Ξ§", "description": "Chi" },
"chi": { "prefix": "\\chi Ο‡", "body": "Ο‡", "description": "chi" },
"Psi": { "prefix": "\\Psi Ξ¨", "body": "Ξ¨", "description": "Psi" },
"psi": { "prefix": "\\psi ψ", "body": "ψ", "description": "psi" },
"Omega": { "prefix": "\\Omega Ξ©", "body": "Ξ©", "description": "Omega" },
"omega": { "prefix": "\\omega Ο‰", "body": "Ο‰", "description": "omega" },
"neg": { "prefix": "\\neg Β¬", "body": "Β¬", "description": "neg" },	
"lnot": { "prefix": "\\lnot Β¬", "body": "Β¬", "description": "lnot" },
"wedge": { "prefix": "\\wedge ∧", "body": "∧", "description": "wedge" },
"land": { "prefix": "\\land ∧", "body": "∧", "description": "land" },
"vee": { "prefix": "\\vee ∨", "body": "∨", "description": "vee" },
"lor": { "prefix": "\\lor ∨", "body": "∨", "description": "lor" },
"parallel": { "prefix": "\\parallel βˆ₯", "body": "βˆ₯", "description": "parallel" },
"oplus": { "prefix": "\\oplus βŠ•", "body": "βŠ•", "description": "oplus" },
"lxor": { "prefix": "\\lxor βŠ•", "body": "βŠ•", "description": "lxor" },
"top": { "prefix": "\\top ⊀", "body": "⊀", "description": "top" },
"bot": { "prefix": "\\bot βŠ₯", "body": "βŠ₯", "description": "bot" },
"forall": { "prefix": "\\forall βˆ€", "body": "βˆ€", "description": "forall" },
"exists": { "prefix": "\\exists βˆƒ", "body": "βˆƒ", "description": "exists" },
"models": { "prefix": "\\models ⊧", "body": "⊧", "description": "models" },
"to": { "prefix": "\\to β†’", "body": "β†’", "description": "to" },
"supset": { "prefix": "\\supset βŠƒ", "body": "βŠƒ", "description": "superset" },
"supseteq": { "prefix": "\\supseteq βŠ‡", "body": "βŠ‡", "description": "supseteq" },
"subset": { "prefix": "\\subset βŠ‚", "body": "βŠ‚", "description": "subset" },
"subseteq": { "prefix": "\\subseteq βŠ†", "body": "βŠ†", "description": "subseteq" },
"nsupset": { "prefix": "\\nsupset βŠ…", "body": "βŠ…", "description": "nsupset" },
"nsubset": { "prefix": "\\nsubset βŠ„", "body": "βŠ„", "description": "nsubset" },
"nsubseteq": { "prefix": "\\nsubset ⊈", "body": "⊈", "description": "nsubset" },
"subsetneq": { "prefix": "\\subsetneq ⊊", "body": "⊊", "description": "subsetneq" },
"nsupseteq": { "prefix": "\\nsupset βŠ‰", "body": "βŠ‰", "description": "nsupset" },
"supsetneq": { "prefix": "\\supsetneq βŠ‹", "body": "βŠ‹", "description": "supsetneq" },
"sqsubset": { "prefix": "\\sqsubset ⊏", "body": "⊏", "description": "sqsubset" },
"sqsupset": { "prefix": "\\sqsupset ⊐", "body": "⊐", "description": "sqsupset" },
"sqsubseteq": { "prefix": "\\sqsubseteq βŠ‘", "body": "βŠ‘", "description": "sqsubseteq" },
"sqsupseteq": { "prefix": "\\sqsupseteq βŠ’", "body": "βŠ’", "description": "sqsupseteq" },
"sqcap": { "prefix": "\\sqcap βŠ“", "body": "βŠ“", "description": "sqcap" },
"sqcup": { "prefix": "\\sqcup βŠ”", "body": "βŠ”", "description": "sqcup" },
"nsqsubseteq": { "prefix": "\\nsqsubset β‹’", "body": "β‹’", "description": "nsqsubset" },
"nsqsupseteq": { "prefix": "\\nsqsupset β‹£", "body": "β‹£", "description": "nsqsupset" },
"sqsubsetneq": { "prefix": "\\sqsubsetneq β‹€", "body": "β‹€", "description": "sqsubsetneq" },
"sqsupsetneq": { "prefix": "\\sqsupsetneq β‹₯", "body": "β‹₯", "description": "sqsupsetneq" },
"equiv": { "prefix": "\\equiv ≑", "body": "≑", "description": "equiv" },
"vDash": { "prefix": "\\vDash ⊨", "body": "⊨", "description": "entails" },
"vdash": { "prefix": "\\vdash ⊒", "body": "⊒", "description": "turnstile" },
"in": { "prefix": "\\in ∈", "body": "∈", "description": "in" },
"ni": { "prefix": "\\ni βˆ‹", "body": "βˆ‹", "description": "ni" },
"notin": { "prefix": "\\notin βˆ‰", "body": "βˆ‰", "description": "notin" },
"notni": { "prefix": "\\notni ∌", "body": "∌", "description": "notni" },
"Rightarrow": { "prefix": "\\Rightarrow β‡’", "body": "β‡’", "description": "Rightarrow" },
"Leftarrow": { "prefix": "\\Leftarrow ⇐", "body": "⇐", "description": "Leftarrow" },
"Uparrow": { "prefix": "\\Uparrow ⇑", "body": "⇑", "description": "Uparrow" },
"Downarrow": { "prefix": "\\Downarrow ⇓", "body": "⇓", "description": "Downarrow" },
"Leftrightarrow": { "prefix": "\\Leftrightarrow ⇔", "body": "⇔", "description": "Leftrightarrow" },
"Updownarrow": { "prefix": "\\Updownarrow ⇕", "body": "⇕", "description": "Updownarrow" },
"uparrow": { "prefix": "\\uparrow ↑", "body": "↑", "description": "uparrow" },
"rightarrow": { "prefix": "\\rightarrow β†’", "body": "β†’", "description": "rightarrow" },
"updownarrow": { "prefix": "\\updownarrow ↕", "body": "↕", "description": "updownarrow" },
"leftrightarrow": { "prefix": "\\leftrightarrow ↔", "body": "↔", "description": "leftrightarrow" },
"twoheadleftarrow": { "prefix": "\\twoheadleftarrow β†ž", "body": "β†ž", "description": "twoheadleftarrow" },
"twoheadrightarrow": { "prefix": "\\twoheadrightarrow β† ", "body": "β† ", "description": "twoheadrightarrow" },
"twoheaduparrow": { "prefix": "\\twoheaduparrow β†Ÿ", "body": "β†Ÿ", "description": "twoheaduparrow" },
"twoheaddownarrow": { "prefix": "\\twoheaddownarrow ↑", "body": "↑", "description": "twoheaddownarrow" },
"approx": { "prefix": "\\approx β‰ˆ", "body": "β‰ˆ", "description": "approx" },
"llbracket": { "prefix": "\\llbracket ⟦", "body": "⟦", "description": "llbracket" },
"rrbracket": { "prefix": "\\rrbracket ⟧", "body": "⟧", "description": "rrbracket" },
"lBrack": { "prefix": "\\lBrack ⟦", "body": "⟦", "description": "lBrack" },
"rBrack": { "prefix": "\\rBrack ⟧", "body": "⟧", "description": "rBrack" }