Last active
August 19, 2022 18:11
-
-
Save Alexander-N/18634441c5fce90f97e30fe0393be008 to your computer and use it in GitHub Desktop.
Substitutions for TLA+ to use with FiraCode
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| { | |
| "conceal.substitutions": [ | |
| { | |
| "language": [ | |
| "tla+", | |
| { | |
| "pattern": "**/*.tla" | |
| } | |
| ], | |
| "substitutions": [ | |
| { | |
| "ugly": "\\\\land", | |
| "pretty": "/\\", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\lor", | |
| "pretty": "\\/", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\equiv", | |
| "pretty": "<=>", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\in", | |
| "post": "\\b", | |
| "pretty": "∈" | |
| }, | |
| { | |
| "ugly": "\\\\notin", | |
| "post": "\\b", | |
| "pretty": "∉" | |
| }, | |
| { | |
| "ugly": "#|/=", | |
| "pretty": "!=" | |
| }, | |
| { | |
| "ugly": "<<", | |
| "pretty": "⟨" | |
| }, | |
| { | |
| "ugly": ">>", | |
| "pretty": "⟩" | |
| }, | |
| { | |
| "ugly": "\\[\\]", | |
| "pretty": "□" | |
| }, | |
| { | |
| "ugly": "\\\\leq", | |
| "pretty": "<=", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "[=][<]", | |
| "pretty": "<=", | |
| }, | |
| { | |
| "ugly": "[<][=]", | |
| "pretty": "<=", | |
| }, | |
| { | |
| "ugly": "\\\\geq", | |
| "pretty": ">=", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "[>][=]", | |
| "pretty": ">=" | |
| }, | |
| { | |
| "ugly": "[~][>]", | |
| "pretty": "~>" | |
| }, | |
| { | |
| "ugly": "~", | |
| "pretty": "¬" | |
| }, | |
| { | |
| "ugly": "\\\\lnot|\\\\neg", | |
| "pretty": "¬", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\ll", | |
| "pretty": "≪", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\gg", | |
| "pretty": "≫", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\preceq", | |
| "pretty": "⪯", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\succeq", | |
| "pretty": "⪰", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\prec", | |
| "pretty": "≺", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\succ", | |
| "pretty": "≻", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "[|][-][>]", | |
| "pretty": "|->" | |
| }, | |
| { | |
| "ugly": "\\\\div", | |
| "pretty": "÷", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\subseteq", | |
| "pretty": "⊆", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\supseteq", | |
| "pretty": "⊇", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\cdot", | |
| "pretty": "⋅", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\subset", | |
| "pretty": "⊂", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\supset", | |
| "pretty": "⊃", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "[(][.][)]", | |
| "pretty": "⊙" | |
| }, | |
| { | |
| "ugly": "\\\\odot", | |
| "pretty": "⊙", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "[(][-][)]", | |
| "pretty": "⊖" | |
| }, | |
| { | |
| "ugly": "\\\\ominus", | |
| "pretty": "⊖", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "[(][+][)]", | |
| "pretty": "⊕" | |
| }, | |
| { | |
| "ugly": "\\\\oplus", | |
| "pretty": "⊕", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "[(][\\\\][X][)]", | |
| "pretty": "⊗" | |
| }, | |
| { | |
| "ugly": "\\\\otimes", | |
| "pretty": "⊗", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "[(][/][)]", | |
| "pretty": "⊘" | |
| }, | |
| { | |
| "ugly": "[(][/][)]|\\\\oslash", | |
| "pretty": "⊘", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\o|\\\\circ", | |
| "pretty": "∘", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\sqsubseteq", | |
| "pretty": "⊑", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\sqsupseteq", | |
| "pretty": "⊒", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\sqsubset", | |
| "pretty": "⊏", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\sqsupset", | |
| "pretty": "⊐", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\bullet", | |
| "pretty": "•", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\star", | |
| "pretty": "⋆", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "[|][-]", | |
| "pretty": "⊢" | |
| }, | |
| { | |
| "ugly": "[-][|]", | |
| "pretty": "⊣" | |
| }, | |
| { | |
| "ugly": "\\\\bigcirc", | |
| "pretty": "◯", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "[|][=]", | |
| "pretty": "⊨" | |
| }, | |
| { | |
| "ugly": "[=][|]", | |
| "pretty": "⫤" | |
| }, | |
| { | |
| "ugly": "\\\\sim", | |
| "pretty": "∼", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "[-][>]", | |
| "pretty": "->" | |
| }, | |
| { | |
| "ugly": "[<][-]", | |
| "pretty": "<-" | |
| }, | |
| { | |
| "ugly": "\\\\simeq", | |
| "pretty": "≃", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\cap|\\\\intersect", | |
| "pretty": "⋂", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\cup|\\\\union", | |
| "pretty": "⋃", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\asymp", | |
| "pretty": "≍", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\sqcap", | |
| "pretty": "⊓", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\sqcup", | |
| "pretty": "⊔", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\approx", | |
| "pretty": "≈", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\uplus", | |
| "pretty": "⨄", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\cong", | |
| "pretty": "≅", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\X|\\\\times", | |
| "pretty": "⨉", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\doteq", | |
| "pretty": "≐", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\wr", | |
| "pretty": "≀", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\propto", | |
| "pretty": "∝", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "\\\\A", | |
| "post": "\\b", | |
| "pretty": "∀" | |
| }, | |
| { | |
| "ugly": "\\\\E", | |
| "post": "\\b", | |
| "pretty": "∃" | |
| }, | |
| { | |
| "ugly": "\\bQED", | |
| "pretty": "∎" | |
| }, | |
| { | |
| "ugly": "Nat", | |
| "pretty": "ℕ", | |
| "pre": "\\b", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "Int", | |
| "pretty": "ℤ", | |
| "pre": "\\b", | |
| "post": "\\b" | |
| }, | |
| { | |
| "ugly": "Real", | |
| "pretty": "ℝ", | |
| "pre": "\\b", | |
| "post": "\\b" | |
| } | |
| ] | |
| } | |
| ] | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
vsc-conceal substitutions for TLA+ adapted from this PR by @teodorov to use together with FiraCode.
I prefer to use larger unicode symbols e.g. ⋃ instead of ∪ and I left out:
{ "ugly": "==", "pretty": "≜" }, { "ugly": "{}", "pretty": "∅" },