Substitutions for TLA+ to use with FiraCode

settings.json

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

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": "∅"
 },