Latex Snippets

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" }