diff --git a/UNRELEASED.md b/UNRELEASED.md
index 84488f67af..1b45f8cb7e 100644
--- a/UNRELEASED.md
+++ b/UNRELEASED.md
@@ -10,3 +10,7 @@
          * Some bug fix, see #124
 
      DO NOT LEAVE A BLANK LINE BELOW THIS PREAMBLE -->
+### Features
+
+* IR: made consistent the names of IR operators (may break JSON compatibility),
+  see #634
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetExpandRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetExpandRule.scala
index d8a633a43b..b7e57d0497 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetExpandRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetExpandRule.scala
@@ -14,7 +14,7 @@ import at.forsyte.apalache.tla.lir.oper.{ApalacheOper, TlaSetOper}
 class SetExpandRule(rewriter: SymbStateRewriter) extends RewritingRule {
   override def isApplicable(symbState: SymbState): Boolean = {
     symbState.ex match {
-      case OperEx(ApalacheOper.expand, OperEx(TlaSetOper.SUBSET, _))    => true
+      case OperEx(ApalacheOper.expand, OperEx(TlaSetOper.powerset, _))  => true
       case OperEx(ApalacheOper.expand, OperEx(TlaSetOper.funSet, _, _)) => true
       case _                                                            => false
     }
@@ -25,7 +25,7 @@ class SetExpandRule(rewriter: SymbStateRewriter) extends RewritingRule {
       case ex @ OperEx(ApalacheOper.expand, OperEx(TlaSetOper.funSet, _, _)) =>
         throw new RewriterException("Trying to expand a set of functions. This will blow up the solver.", ex)
 
-      case ex @ OperEx(ApalacheOper.expand, OperEx(TlaSetOper.SUBSET, basesetEx)) =>
+      case ex @ OperEx(ApalacheOper.expand, OperEx(TlaSetOper.powerset, basesetEx)) =>
         var nextState = rewriter.rewriteUntilDone(state.setRex(basesetEx))
         new PowSetCtor(rewriter).confringo(nextState, nextState.asCell)
 
diff --git a/tla-import/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporter.scala b/tla-import/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporter.scala
index 760fed9840..20c5d99634 100644
--- a/tla-import/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporter.scala
+++ b/tla-import/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporter.scala
@@ -612,7 +612,7 @@ class TestSanyImporter extends FunSuite with BeforeAndAfter {
         "Implies",
         OperEx(TlaBoolOper.implies, ValEx(TlaBool(false)), ValEx(TlaBool(true)))
     )
-    expectDecl("Subset", OperEx(TlaSetOper.SUBSET, NameEx("x")))
+    expectDecl("Subset", OperEx(TlaSetOper.powerset, NameEx("x")))
     expectDecl("Union", OperEx(TlaSetOper.union, NameEx("x")))
     expectDecl("Domain", OperEx(TlaFunOper.domain, NameEx("x")))
     expectDecl(
diff --git a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala
index 7de75b66b0..348c423ad3 100644
--- a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala
+++ b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala
@@ -337,7 +337,7 @@ class ToEtcExpr(annotationStore: AnnotationStore, aliasSubstitution: ConstSubsti
         val opsig = OperT1(List(SetT1(a), SetT1(a)), BoolT1())
         mkExRefApp(opsig, args)
 
-      case OperEx(TlaSetOper.SUBSET, args @ _*) =>
+      case OperEx(TlaSetOper.powerset, args @ _*) =>
         // SUBSET S
         val a = varPool.fresh
         val opsig = OperT1(List(SetT1(a)), SetT1(SetT1(a)))
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaActionOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaActionOper.scala
index 4c5d33b571..66f96f9929 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaActionOper.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaActionOper.scala
@@ -13,7 +13,7 @@ object TlaActionOper {
    * The prime operator. By the TLA+ restrictions, we cannot apply it twice, e.g., (x')' is illegal.
    */
   object prime extends TlaActionOper {
-    override val name: String = "'"
+    override val name: String = "PRIME"
 
     override def arity: OperArity = FixedArity(1)
 
@@ -21,10 +21,10 @@ object TlaActionOper {
   }
 
   /**
-   * The operator that executes an action or keeps the variable values.
+   * The operator that executes an action or keeps the variable values. It has the form `[A]_e`.
    */
   object stutter extends TlaActionOper {
-    override val name: String = "[A]_e"
+    override val name: String = "STUTTER"
 
     override def arity: OperArity = FixedArity(2)
 
@@ -32,10 +32,10 @@ object TlaActionOper {
   }
 
   /**
-   * The operator that executes an action and enforces the values to change.
+   * The operator that executes an action and enforces the values to change. It has the form `<A>_e`.
    */
   object nostutter extends TlaActionOper {
-    override val name: String = "<A>_e"
+    override val name: String = "NO_STUTTER"
 
     override def arity: OperArity = FixedArity(2)
 
@@ -65,13 +65,10 @@ object TlaActionOper {
   }
 
   /**
-   * The sequential composition of operators.
-   *
-   * Jure@17.11.16: Arity 2?
-   * Igor@12.03.17: Arity 2. Fixed.
+   * The sequential composition of operators, which usually has the name `\cdot`.
    */
   object composition extends TlaActionOper {
-    override val name: String = "\\cdot"
+    override val name: String = "COMPOSE"
     override def arity: OperArity = FixedArity(2)
     override def precedence: (Int, Int) = (13, 13)
   }
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaArithOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaArithOper.scala
index 5ab17b862b..9017f13517 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaArithOper.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaArithOper.scala
@@ -27,123 +27,133 @@ abstract class TlaArithOper extends TlaOper {
 object TlaArithOper {
 
   /**
-   * A binary addition.
+   * A binary addition: `a + b`.
    */
   object plus extends TlaArithOper {
     override val arity = FixedArity(2)
-    override val name = "(+)"
+    override val name = "PLUS"
     override val precedence: (Int, Int) = (10, 10)
   }
 
   /**
-   * A unary minus. Note that Naturals do not have unary minus.
+   * A unary minus: `-a`. Note that Naturals do not have unary minus.
    */
   object uminus extends TlaArithOper {
     override val arity = FixedArity(1)
-    override val name = "-."
+    override val name = "UNARY_MINUS"
     override val precedence: (Int, Int) = (12, 12)
   }
 
   /**
-   * A binary minus.
+   * A binary minus: `a - b`.
    */
   object minus extends TlaArithOper {
     override val arity = FixedArity(2)
-    override val name = "(-)"
+    override val name = "MINUS"
     override val precedence: (Int, Int) = (11, 11)
   }
 
   /**
-   * A multiplication.
+   * A multiplication: `a * b`.
    */
   object mult extends TlaArithOper {
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "(*)"
+
+    override val name: String = "MULT"
     override val precedence: (Int, Int) = (13, 13)
   }
 
   /**
-   * Integer division.
+   * Integer division: `a \div b`.
    */
   object div extends TlaArithOper {
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "(\\div)"
+
+    override val name: String = "DIV"
     override val precedence: (Int, Int) = (13, 13)
   }
 
   /**
-   * Remainder of an integer division.
+   * Remainder of an integer division: `a % b`
    */
   object mod extends TlaArithOper {
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "(%)"
+
+    override val name: String = "MOD"
     override val precedence: (Int, Int) = (10, 11)
   }
 
   /**
-   * Real division.
+   * Real division, defined in `Reals`: `a / b`
    */
   object realDiv extends TlaArithOper {
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "(/)"
+
+    override val name: String = "REAL_DIV"
     override val precedence: (Int, Int) = (13, 13)
   }
 
   /**
-   * Exponent, i.e., x^y gives us x multiplied by itself (y-1) times.
+   * Exponent, i.e., `x^y` gives us `x` multiplied by itself `y - 1` times.
    */
   object exp extends TlaArithOper {
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "(^)"
+
+    override val name: String = "POW"
     override val precedence: (Int, Int) = (14, 14)
   }
 
   /**
-   * An integer/natural range, that is, a..b = {a,...,b}
+   * An integer/natural range as a set: `a..b`. Both `a` and `b` are included. It can be understood as
+   * `{ i \in Int: a <= i /\ i <= b }`.
    */
   object dotdot extends TlaArithOper {
     override val arity = FixedArity(2)
-    override val name = "_.._"
+    override val name = "INT_RANGE"
     override val precedence: (Int, Int) = (9, 9)
   }
 
   /**
-   * Less than.
+   * Less than: `a < b`.
    */
   object lt extends TlaArithOper {
     /* the number of arguments the operator has */
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "(<)"
+
+    override val name: String = "LT"
     override val precedence: (Int, Int) = (5, 5)
   }
 
   /**
-   * Greater than.
+   * Greater than: `a > b`.
    */
   object gt extends TlaArithOper {
     /* the number of arguments the operator has */
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "(>)"
+
+    override val name: String = "GT"
     override val precedence: (Int, Int) = (5, 5)
   }
 
   /**
-   * Less than or equals.
+   * Less than or equals: `a <= b`.
    */
   object le extends TlaArithOper {
     /* the number of arguments the operator has */
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "(<=)"
+
+    override val name: String = "LE"
     override val precedence: (Int, Int) = (5, 5)
   }
 
   /**
-   * Greater than or equals.
+   * Greater than or equals: `a >= b`.
    */
   object ge extends TlaArithOper {
     /* the number of arguments the operator has */
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "(>=)"
+
+    override val name: String = "GE"
     override val precedence: (Int, Int) = (5, 5)
   }
 }
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaBoolOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaBoolOper.scala
index 8eb2759c46..7d40febd2f 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaBoolOper.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaBoolOper.scala
@@ -18,7 +18,7 @@ object TlaBoolOper {
    */
   object and extends TlaBoolOper {
     override def arity = AnyArity()
-    override val name = "/\\"
+    override val name = "AND"
     override val precedence: (Int, Int) = (3, 3)
   }
 
@@ -30,7 +30,8 @@ object TlaBoolOper {
    */
   object or extends TlaBoolOper {
     override def arity: OperArity = AnyArity()
-    override val name: String = "\\/"
+
+    override val name: String = "OR"
     override val precedence: (Int, Int) = (3, 3)
   }
 
@@ -39,7 +40,8 @@ object TlaBoolOper {
    */
   object not extends TlaBoolOper {
     override def arity: OperArity = FixedArity(1)
-    override val name: String = "~"
+
+    override val name: String = "NOT"
     override val precedence: (Int, Int) = (4, 4)
   }
 
@@ -48,7 +50,8 @@ object TlaBoolOper {
    */
   object implies extends TlaBoolOper {
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "=>"
+
+    override val name: String = "IMPLIES"
     override val precedence: (Int, Int) = (1, 1)
   }
 
@@ -57,35 +60,48 @@ object TlaBoolOper {
    */
   object equiv extends TlaBoolOper {
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "<=>"
+
+    override val name: String = "EQUIV"
     override val precedence: (Int, Int) = (2, 2)
   }
 
-  /** \A x \in S : p */
+  /**
+   * A universal quantifier over a set: `\A x \in S : p`.
+   */
   object forall extends TlaBoolOper {
     override def arity: OperArity = FixedArity(3)
-    override val name: String = "\\A3"
+
+    override val name: String = "FORALL3"
     override val precedence: (Int, Int) = (0, 0) // Section 15.2.1
   }
 
-  /** \A x : p */
+  /**
+   * A universal quantifier over the whole universe: `\A x : p`.
+   */
   object forallUnbounded extends TlaBoolOper {
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "\\A2"
+
+    override val name: String = "FORALL2"
     override val precedence: (Int, Int) = (0, 0) // Section 15.2.1
   }
 
-  /** \E x \in S : p */
+  /**
+   * An existential quantifier over a set: `\E x \in S : p`.
+   */
   object exists extends TlaBoolOper {
     override def arity: OperArity = FixedArity(3)
-    override val name: String = "\\E3"
+
+    override val name: String = "EXISTS3"
     override val precedence: (Int, Int) = (0, 0) // Section 15.2.1
   }
 
-  /** \E x : p */
+  /**
+   * An existential quantifier over the whole universe: `\E x : p`.
+   */
   object existsUnbounded extends TlaBoolOper {
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "\\E2"
+
+    override val name: String = "EXISTS2"
     override val precedence: (Int, Int) = (0, 0) // Section 15.2.1
   }
 }
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaControlOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaControlOper.scala
index c41a710bf6..4797322214 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaControlOper.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaControlOper.scala
@@ -29,7 +29,7 @@ object TlaControlOper {
    * The rationale is that by using args.tail, one obtains a list similar to the caseOper.
    */
   object caseWithOther extends TlaControlOper {
-    override val name: String = "CASE-OTHER"
+    override val name: String = "CASE_OTHER"
     override val arity: OperArity = MinimalArity(3) && AnyOddArity() //new OperArity( k => k >= 3 && k % 2 == 1 )
     override val interpretation: Interpretation.Value = Interpretation.Predefined
     override val precedence: (Int, Int) = (0, 0)
@@ -39,7 +39,7 @@ object TlaControlOper {
    * The "IF A THEN B ELSE C" operator. The arguments have the following structure: A, B, C.
    */
   object ifThenElse extends TlaControlOper {
-    override val name: String = "IF-THEN-ELSE"
+    override val name: String = "IF_THEN_ELSE"
     override val arity: OperArity = FixedArity(3)
     override val interpretation: Interpretation.Value = Interpretation.Predefined
     override val precedence: (Int, Int) = (0, 0)
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaFiniteSetOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaFiniteSetOper.scala
index df238d1577..382699aecd 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaFiniteSetOper.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaFiniteSetOper.scala
@@ -12,20 +12,20 @@ abstract class TlaFiniteSetOper extends TlaOper {
 object TlaFiniteSetOper {
 
   /**
-   * The operator that checks, whether a set is finite.
+   * The operator that checks, whether a set is finite: `IsFiniteSet(S)`.
    */
   object isFiniteSet extends TlaFiniteSetOper {
     override val arity = FixedArity(1)
-    override val name = "IsFiniteSet"
+    override val name = "FiniteSets!IsFiniteSet"
     override val precedence: (Int, Int) = (16, 16) // as the function application
   }
 
   /**
-   * The operator that returns the cardinality of a finite set.
+   * The operator that returns the cardinality of a finite set: `Cardinality(S)`.
    */
   object cardinality extends TlaFiniteSetOper {
     override val arity = FixedArity(1)
-    override val name = "Cardinality"
+    override val name = "FiniteSets!Cardinality"
     override val precedence: (Int, Int) = (16, 16) // as the function application
   }
 
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaFunOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaFunOper.scala
index d5db3aceb2..13f2eb245f 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaFunOper.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaFunOper.scala
@@ -10,37 +10,43 @@ abstract class TlaFunOper extends TlaOper {
 object TlaFunOper {
 
   /**
-   * A function constructor like the one for the records: [ k_1 |-> v_1, ..., k_n |-> v_n ].
+   * <p>A function constructor like the one for the records: [ k_1 |-> v_1, ..., k_n |-> v_n ].
    * The order of the arguments is: (k_1, v_1, ..., k_n, v_n).
-   * Note that in case of records, k_1, ..., k_n are strings, that is, ValEx(TlaStr(...)), not NameEx.
+   * Note that in case of records, k_1, ..., k_n are strings, that is, ValEx(TlaStr(...)), not NameEx.</p>
+   *
+   * <p>Although this constructor could be used for functions in general, it is used only for the records in TLA+.
+   * That is why we call it "REC_CTOR".</p>
    */
   object enum extends TlaFunOper {
     override def arity: OperArity = new OperArity(k => k >= 2 && k % 2 == 0)
-    override val name: String = "fun-enum"
+
+    override val name: String = "RECORD"
     override val precedence: (Int, Int) = (16, 16) // as the function application
   }
 
   /**
-   * Define a tuple by listing its elements, i.e., < e_1, ..., e_k >.
-   * One can use enum to achieve the same effect.
+   * Define a tuple by listing its elements: `<< e_1, ..., e_k >>`.
+   * Note that tuples are indistinguishable from sequences in pure TLA+, this can also be used to construct a sequence.
    */
   object tuple extends TlaFunOper {
     override val arity = AnyArity()
-    override val name = "<<...>>"
+    override val name = "TUPLE"
     override val precedence: (Int, Int) = (16, 16) // as the function application
   }
 
   /**
-   * A function application, e.g., f[e].
+   * A function application: `f[e]`. Note that `f` can be: a function, a record, a tuple, or a sequence.
    * The order of the arguments is: (f, e).
    */
   object app extends TlaFunOper {
     override val arity: OperArity = FixedArity(2)
-    override val name: String = "fun-app"
+    override val name: String = "FUN_APP"
     override val precedence: (Int, Int) = (16, 16)
   }
 
-  /** DOMAIN f */
+  /**
+   * A function domain: `DOMAIN f`. Note that `f` can be: a function, a record, a tuple, or a sequence.
+   */
   object domain extends TlaFunOper {
     override val arity: OperArity = FixedArity(1)
     override val name: String = "DOMAIN"
@@ -48,18 +54,19 @@ object TlaFunOper {
   }
 
   /**
-   * A function constructor: [ x \in S |-> e ]. In fact, it is a lambda function (NOT the TLA+ LAMBDA!)
-   * Similar to \E and \A, one can use many combinations of variables and tuples, e.g.,
-   * [ x, y \in S, <<a, b>> \in S |-> e ]. We translate function constructors
+   * A function constructor: `[ x \in S |-> e ]`. In fact, it is a lambda function (NOT the TLA+ LAMBDA!)
+   * Similar to `\E` and `\A`, one can use many combinations of variables and tuples, e.g.,
+   * `[ x, y \in S, <<a, b>> \in S |-> e ]`. We translate function constructors
    * in a list of fixed structure, where the defining expression comes first and every variables (or a tuple)
-   * comes with its bounding set, e.g., (e, x, S, y, S, <<a, b>>, S).
+   * comes with its bounding set, e.g., `(e, x, S, y, S, <<a, b>>, S)`.
    *
-   * The arguments are always an odd-length list
-   * of the following structure: body, x_1, S_1, ..., x_k, S_k.
+   * <p>The arguments are always an odd-length list
+   * of the following structure: body, x_1, S_1, ..., x_k, S_k.</p>
    */
   object funDef extends TlaFunOper {
     override def arity: OperArity = new OperArity(k => k >= 3 && k % 2 == 1)
-    override val name: String = "fun-def"
+
+    override val name: String = "FUN_CTOR"
     override val precedence: (Int, Int) = (16, 16) // as the function application
   }
 
@@ -114,7 +121,9 @@ object TlaFunOper {
    */
   object recFunDef extends TlaFunOper {
     override def arity: OperArity = new OperArity(_ >= 3)
-    override def name: String = "rec-fun-def"
+
+    override def name: String = "FUN_REC_CTOR"
+
     override def precedence: (Int, Int) = (100, 100) // as the operator declaration
   }
 
@@ -129,7 +138,9 @@ object TlaFunOper {
      * A unique name that can be used to refer to a recursive function inside its body.
      */
     val uniqueName = "$recFun"
-    override def name: String = "rec-fun-ref"
+
+    override def name: String = "FUN_REC_REF"
+
     override def arity: OperArity = FixedArity(0)
     override def precedence: (Int, Int) = (16, 16) // as function application
   }
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaOper.scala
index 626e4b9722..2049f4232a 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaOper.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaOper.scala
@@ -59,8 +59,9 @@ object TlaOper {
 
   /**
    * Group two lists of arguments into a single interleaved list, starting with the head of even.
+   *
    * @param even the list of even arguments
-   * @param odd the list of odd arguments
+   * @param odd  the list of odd arguments
    * @return the interleaved list
    */
   def interleave(even: Seq[TlaEx], odd: Seq[TlaEx]): Seq[TlaEx] = {
@@ -70,17 +71,21 @@ object TlaOper {
     }
   }
 
-  /** Equality of two TLA+ objects */
+  /**
+   * Equality of two TLA+ objects: `a = b`.
+   */
   object eq extends TlaOper {
-    val name = "="
+    val name = "EQ"
     val interpretation: Interpretation.Value = Interpretation.Predefined
     val arity = FixedArity(2)
     override val precedence: (Int, Int) = (5, 5)
   }
 
-  /** Inequality of two TLA+ objects */
+  /**
+   * Inequality of two TLA+ objects: `a /= b`.
+   */
   object ne extends TlaOper {
-    val name = "/="
+    val name = "NE"
     val interpretation: Interpretation.Value = Interpretation.Predefined
     val arity = FixedArity(2)
     override val precedence: (Int, Int) = (5, 5)
@@ -126,12 +131,13 @@ object TlaOper {
     override def arity: OperArity = AnyPositiveArity()
 
     override def interpretation: Interpretation.Value = Interpretation.Predefined
-    override val name: String = "_()"
+
+    override val name: String = "OPER_APP"
     override val precedence: (Int, Int) = (16, 16)
   }
 
   /**
-   * The CHOOSE operator: CHOOSE x \in S: p
+   * Choose from a set: `CHOOSE x \in S: p`
    */
   object chooseBounded extends TlaOper {
     // TODO: move this operator to TlaBoolOper? (Igor)
@@ -146,7 +152,7 @@ object TlaOper {
   }
 
   /**
-   * The CHOOSE operator: CHOOSE x : p
+   * Choose from the universe: `CHOOSE x : p`
    */
   object chooseUnbounded extends TlaOper {
     // TODO: move this operator to TlaBoolOper? (Igor)
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaSeqOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaSeqOper.scala
index adf67b2e49..65089bc4ee 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaSeqOper.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaSeqOper.scala
@@ -1,11 +1,11 @@
 package at.forsyte.apalache.tla.lir.oper
 
 /**
- * Sequence operators
+ * Sequence operators.
  *
  * @author Jure Kukovec
  *
- * Created by jkukovec on 11/17/16.
+ *         Created by jkukovec on 11/17/16.
  */
 
 abstract class TlaSeqOper extends TlaOper {
@@ -20,43 +20,43 @@ object TlaSeqOper {
 
   object head extends TlaSeqOper {
     override val arity = FixedArity(1)
-    override val name = "Head"
+    override val name = "Sequences!Head"
     override val precedence: (Int, Int) = (16, 16) // as the function application
   }
 
   object tail extends TlaSeqOper {
     override val arity = FixedArity(1)
-    override val name = "Tail"
+    override val name = "Sequences!Tail"
     override val precedence: (Int, Int) = (16, 16) // as the function application
   }
 
   object append extends TlaSeqOper {
     override val arity = FixedArity(2)
-    override val name = "Append"
+    override val name = "Sequences!Append"
     override val precedence: (Int, Int) = (16, 16) // as the function application
   }
 
   object concat extends TlaSeqOper {
     override val arity = FixedArity(2)
-    override val name = "\\o"
+    override val name = "Sequences!Concat"
     override val precedence: (Int, Int) = (13, 13)
   }
 
   object len extends TlaSeqOper {
     override val arity = FixedArity(1)
-    override val name = "Len"
+    override val name = "Sequences!Len"
     override val precedence: (Int, Int) = (16, 16) // as the function application
   }
 
   object subseq extends TlaSeqOper {
     override val arity = FixedArity(3)
-    override val name = "SubSeq"
+    override val name = "Sequences!SubSeq"
     override val precedence: (Int, Int) = (16, 16) // as the function application
   }
 
   object selectseq extends TlaSeqOper {
     override val arity = FixedArity(2)
-    override val name = "SelectSeq"
+    override val name = "Sequences!SelectSeq"
     override val precedence: (Int, Int) = (16, 16) // as the function application
   }
 }
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaSetOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaSetOper.scala
index 49887f6947..ac8e6b795c 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaSetOper.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaSetOper.scala
@@ -10,34 +10,34 @@ abstract class TlaSetOper extends TlaOper {
 object TlaSetOper {
 
   /**
-   *  Define a set by enumerating its elements, i.e., {e_1, ..., e_k}
-   *    Note that we explicitly forbid to construct an empty set using this operator.
-   *    To construct an empty set, use emptySet.
+   * Define a set by enumerating its elements: `{e_1, ..., e_k}`.
    */
   object enumSet extends TlaSetOper {
-    override val arity = AnyArity() // FIX: we allow zero arguments as well
-    override val name = "{...}"
+    override val arity = AnyArity()
+    override val name = "SET_ENUM"
     override val precedence: (Int, Int) = (16, 16) // as the function application
   }
 
   /**
-   * Construct a set of functions from a set S to a set T, i.e., [S -> T].
+   * Construct a set of functions from a set S to a set T, that is, `[S -> T]`.
    */
   object funSet extends TlaSetOper {
     override def arity: OperArity = FixedArity(2)
-    override val name: String = "[S -> T]"
+
+    override val name: String = "FUN_SET"
     override val precedence: (Int, Int) = (16, 16) // as the function application
   }
 
   /**
-   * Construct a set of records, e.g., [ f_1: S_1, ..., f_k: S_k ].
-   * The order of the arguments is as follows: (f_1, S_1, ..., f_k, S_k).
-   * The field names f_1, ..., f_k are string constants,
-   * that is, ValEx(TlaStr("...")) and not NameEx("...")
+   * Construct a set of records, e.g., `[ f_1: S_1, ..., f_k: S_k ]`.
+   * The order of the arguments is as follows: `(f_1, S_1, ..., f_k, S_k)`.
+   * The field names `f_1`, ..., `f_k`` are string constants,
+   * that is, `ValEx(TlaStr("..."))` and not `NameEx("...")`.
    */
   object recSet extends TlaSetOper {
     override def arity: OperArity = AnyEvenArity()
-    override val name: String = "$SetOfRcds"
+
+    override val name: String = "RECORD_SET"
     override val precedence: (Int, Int) = (16, 16) // as the function application
   }
 
@@ -46,110 +46,113 @@ object TlaSetOper {
    */
   object seqSet extends TlaSetOper {
     override def arity: OperArity = FixedArity(1)
-    override val name: String = "Seq"
+
+    override val name: String = "Sequences!Seq"
     override val precedence: (Int, Int) = (16, 16) // as the function application
   }
 
+  /**
+   * Set membership: `e \in S`.
+   */
   object in extends TlaSetOper {
     override val arity = FixedArity(2)
-    override val name = "\\in"
+    override val name = "SET_IN"
     override val precedence: (Int, Int) = (5, 5)
   }
 
+  /**
+   * Set non-membership: `e \notin S`.
+   */
   object notin extends TlaSetOper {
     override val arity = FixedArity(2)
-    override val name = "\\notin"
+    override val name = "SET_NOT_IN"
     override val precedence: (Int, Int) = (5, 5)
   }
 
+  /**
+   * Set union, that is, `S \\union T` or `S \cup T`.
+   */
   object cup extends TlaSetOper {
     override val arity = FixedArity(2)
-    override val name = "\\union"
+    override val name = "SET_UNION2"
     override val precedence: (Int, Int) = (8, 8)
   }
 
+  /**
+   * Set intersection, that is, `S \intersect T` or `S \cap T`.
+   */
   object cap extends TlaSetOper {
     override val arity = FixedArity(2)
-    override val name = "\\intersect"
+    override val name = "SET_INTERSECT"
     override val precedence: (Int, Int) = (8, 8)
   }
 
-  /** the standard \subseteq operator */
+  /**
+   * Subset-or-equals: `S \subseteq T`.
+   */
   object subseteq extends TlaSetOper {
     override val arity = FixedArity(2)
-    override val name = "\\subseteq"
+    override val name = "SET_SUBSET_EQ"
     override val precedence: (Int, Int) = (5, 5)
   }
 
-  /** the standard set difference */
+  /**
+   * Set difference, that is, `S \setminus T`.
+   */
   object setminus extends TlaSetOper {
     override val arity = FixedArity(2)
-    override val name = "\\setminus"
+    override val name = "SET_MINUS"
     override val precedence: (Int, Int) = (8, 8)
   }
 
   /**
-   * A restricted set comprehension: { x \in S : p }.
-   * The argument order is: (x, S, p). Note that x may be a tuple.
+   * A restricted set comprehension: `{ x \in S : p }`.
+   * The argument order is: `(x, S, p)`. Note that x may be a tuple.
    */
   object filter extends TlaSetOper {
-    // Jure, 24.11.2017:
-    // Should we unify notation with TlaFunOper.funDef? funDef has args (e, (x, S)+ )
-    //
-    // Igor @ 19.12.2018: What's the point? The only use of multiple parameters,
-    // is to filter a Cartesian product. In this case, one can directly pass a Cartesian
-    // product as an argument. The tuple gives us some form of primitive pattern matching.
     override val arity = FixedArity(3)
-    override val name = "filter"
+    override val name = "SET_FILTER"
     override val precedence: (Int, Int) = (16, 16)
   }
 
   /**
-   * A set mapping: { e: x_1 \in S_1, ..., x_k \in S_k }.
-   * The argument order is: (e, x_1, S_1, ..., x_k, S_k)
+   * A set mapping: `{ e: x_1 \in S_1, ..., x_k \in S_k }`.
+   * The argument order is: `(e, x_1, S_1, ..., x_k, S_k)`.
    */
   object map extends TlaSetOper {
     override val arity = new OperArity(k => k >= 3 && k % 2 == 1)
-    override val name = "map"
+    override val name = "SET_MAP"
     override val precedence: (Int, Int) = (16, 16)
   }
 
   /**
-   * TLA SUBSET, i.e., the set of all subsets (of a given set).
-   *    We use the name 'powerset' to avoid confusion with \subset and \subseteq.
+   * The set of all subsets (of a given set): `SUBSET S`.
+   * We use the name 'SET_POWERSET' to avoid confusion with `SET_SUBSET_EQ`.
    */
   object powerset extends TlaSetOper {
     override val arity = FixedArity(1)
-    override val name = "SUBSET"
+    override val name = "SET_POWERSET"
     override val precedence: (Int, Int) = (8, 8)
   }
 
   /**
-   * An alias for powerset, as TLA+ has this (rather confusing) keyword for the powerset.
-   *
-   * WARNING: Do not confuse with subsetProper, that is, a proper subset relation.
-   */
-  val SUBSET: TlaSetOper = powerset
-
-  /**
-   * TLA UNION, i.e., the union of all elements (of a given set).
-   *
-   *    WARNING: use it when you really need it. In all other cases, use \cup.
+   * The union of all elements (of a given set): `UNION S`.
+   * This operator should not confused with `S \\union T`.
    */
   object union extends TlaSetOper {
     override val arity = FixedArity(1)
-    override val name = "UNION"
+    override val name = "SET_UNARY_UNION"
     override val precedence: (Int, Int) = (8, 8)
   }
 
   /**
-   *    Define a cartesian product of one or more sets.
-   *    Note that we explicitly forbid to construct an empty set using this operator.
-   *    To construct an empty set, use enumSet with no arguments.
+   * Define a cartesian product of one or more sets.
+   * Note that we explicitly forbid to construct an empty set using this operator.
+   * To construct an empty set, use `enumSet` with no arguments.
    */
   object times extends TlaSetOper {
     override val arity = AnyArity()
-    override val name = "\\times"
+    override val name = "SET_TIMES"
     override val precedence: (Int, Int) = (10, 13)
   }
 }
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaTempOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaTempOper.scala
index cd30455c2e..ddb4bbb62c 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaTempOper.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaTempOper.scala
@@ -9,63 +9,89 @@ abstract class TlaTempOper extends TlaOper {
 
 object TlaTempOper {
 
-  /** The LTL box operator */
+  /**
+   * The LTL box operator: `[]P`.
+   */
   object box extends TlaTempOper {
-    override val name: String = "[]"
+    override val name: String = "GLOBALLY"
+
     override def arity: OperArity = FixedArity(1)
+
     override val precedence: (Int, Int) = (4, 15)
   }
 
-  /** The LTL diamond operator */
+  /**
+   * The LTL diamond operator: `<>P`.
+   */
   object diamond extends TlaTempOper {
-    override val name: String = "<>"
+    override val name: String = "EVENTUALLY"
+
     override def arity: OperArity = FixedArity(1)
+
     override val precedence: (Int, Int) = (4, 15)
   }
 
-  /** The leads-to operator */
+  /**
+   * The leads-to operator: `P ~> Q`.
+   */
   object leadsTo extends TlaTempOper {
-    override val name: String = "~>"
+    override val name: String = "LEADS_TO"
+
     override def arity: OperArity = FixedArity(2)
+
     override val precedence: (Int, Int) = (2, 2)
   }
 
-  /** The 'guarantees' operator */
+  /**
+   * The 'guarantees' operator: `P -+-> Q`.
+   */
   object guarantees extends TlaTempOper {
-    override val name: String = "-+->"
+    override val name: String = "GUARANTEES"
+
     override def arity: OperArity = FixedArity(2)
+
     override val precedence: (Int, Int) = (2, 2)
   }
 
   /**
-   * The weak fairness operator WF_x(A). The argument order is: (x, A).
+   * The weak fairness operator: `WF_x(A)`. The argument order is: (x, A).
    */
   object weakFairness extends TlaTempOper {
-    override val name: String = "WF"
+    override val name: String = "WEAK_FAIRNESS"
     override def arity: OperArity = FixedArity(2)
     override val precedence: (Int, Int) = (4, 15)
   }
 
   /**
-   * The strong fairness operator SF_x(A). The argument order is: (x, A)
+   * The strong fairness operator: `SF_x(A)`. The argument order is: (x, A)
    */
   object strongFairness extends TlaTempOper {
-    override val name: String = "SF"
+    override val name: String = "STRONG_FAIRNESS"
+
     override def arity: OperArity = FixedArity(2)
+
     override val precedence: (Int, Int) = (4, 15)
   }
 
-  /** The temporal existential quantification (hiding) operator */
+  /**
+   * The temporal existential quantification (hiding) operator: `\EE x: P`.
+   */
   object EE extends TlaTempOper {
-    override val name: String = "\\EE"
+    override val name: String = "TEMPORAL_EXISTS"
+
     override def arity: OperArity = FixedArity(2)
+
     override val precedence: (Int, Int) = (0, 0) // Sec 15.2.1, Undelimited Constructs
   }
 
-  /** The temporal universal quantification operator */
+  /**
+   * The temporal universal quantification operator: `\AA x: P`.
+   */
   object AA extends TlaTempOper {
-    override val name: String = "\\AA"
+    override val name: String = "TEMPORAL_FORALL"
+
     override def arity: OperArity = FixedArity(2)
+
     override val precedence: (Int, Int) = (0, 0) // Sec 15.2.1, Undelimited Constructs
   }
 }
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlcOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlcOper.scala
index 7a9350453e..574a0e6ab6 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlcOper.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlcOper.scala
@@ -12,7 +12,7 @@ abstract class TlcOper extends TlaOper {
 object TlcOper {
 
   /**
-   * Print(out, val) from TLC.
+   * Operator `Print(out, val)` from TLC.
    */
   object print extends TlcOper {
     override def name: String = "TLC!Print"
@@ -21,7 +21,7 @@ object TlcOper {
   }
 
   /**
-   * PrintT(out) from TLC.
+   * Operator `PrintT(out)` from TLC.
    */
   object printT extends TlcOper {
     override def name: String = "TLC!PrintT"
@@ -30,7 +30,7 @@ object TlcOper {
   }
 
   /**
-   * Assert(out, val) from TLC.
+   * Operator `Assert(out, val)` from TLC.
    */
   object assert extends TlcOper {
     override def name: String = "TLC!Assert"
@@ -39,7 +39,7 @@ object TlcOper {
   }
 
   /**
-   * JavaTime from TLC.
+   * Operator `JavaTime` from TLC.
    */
   object javaTime extends TlcOper {
     override def name: String = "TLC!javaTime"
@@ -48,7 +48,7 @@ object TlcOper {
   }
 
   /**
-   * TLCGet(i) from TLC.
+   * Operator `TLCGet(i)` from TLC.
    */
   object tlcGet extends TlcOper {
     override def name: String = "TLC!TLCGet"
@@ -57,7 +57,7 @@ object TlcOper {
   }
 
   /**
-   * TLCSet(i, v) from TLC.
+   * Operator `TLCSet(i, v)` from TLC.
    */
   object tlcSet extends TlcOper {
     override def name: String = "TLC!TLCSet"
@@ -66,7 +66,7 @@ object TlcOper {
   }
 
   /**
-   * _ :> _ from TLC.
+   * Singleton function in TLC: `a :> b`.
    */
   object colonGreater extends TlcOper {
     override def name: String = "TLC!:>"
@@ -75,7 +75,7 @@ object TlcOper {
   }
 
   /**
-   * _ @@ _ from TLC.
+   * Function concatenation in TLC: `f @@ g`.
    */
   object atat extends TlcOper {
     override def name: String = "TLC!@@"
@@ -84,7 +84,7 @@ object TlcOper {
   }
 
   /**
-   * Permutations(S) from TLC.
+   * Operator `Permutations(S)` from TLC.
    */
   object permutations extends TlcOper {
     override def name: String = "TLC!Permutations"
@@ -93,7 +93,7 @@ object TlcOper {
   }
 
   /**
-   * SortSeq(s, Op(_, _)) from TLC.
+   * Operator `SortSeq(s, Op(_, _))` from TLC.
    */
   object sortSeq extends TlcOper {
     override def name: String = "TLC!SortSeq"
@@ -102,7 +102,7 @@ object TlcOper {
   }
 
   /**
-   * RandomElement(S) from TLC.
+   * Operator `RandomElement(S)` from TLC.
    */
   object randomElement extends TlcOper {
     override def name: String = "TLC!RandomElement"
@@ -111,7 +111,7 @@ object TlcOper {
   }
 
   /**
-   * any from TLC.
+   * Operator `Any` from TLC.
    */
   object any extends TlcOper {
     override def name: String = "TLC!Any"
@@ -120,7 +120,7 @@ object TlcOper {
   }
 
   /**
-   * ToString(S) from TLC.
+   * Operator `ToString(S)` from TLC.
    */
   object tlcToString extends TlcOper {
     override def name: String = "TLC!ToString"
@@ -129,7 +129,7 @@ object TlcOper {
   }
 
   /**
-   * TLCEval(v) from TLC.
+   * Operator `TLCEval(v)` from TLC.
    */
   object tlcEval extends TlcOper {
     override def name: String = "TLC!TLCEval"
diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestPrettyWriter.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestPrettyWriter.scala
index 99c41c3a20..bdc15226e5 100644
--- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestPrettyWriter.scala
+++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/io/TestPrettyWriter.scala
@@ -643,12 +643,12 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach {
     assert(expected == stringWriter.toString)
   }
 
-  test("Cardinality") {
+  test("FiniteSets!Cardinality") {
     val writer = new PrettyWriter(printWriter, 80)
     val expr = card(name("S"))
     writer.write(expr)
     printWriter.flush()
-    val expected = """Cardinality(S)""".stripMargin
+    val expected = """FiniteSets!Cardinality(S)""".stripMargin
     assert(expected == stringWriter.toString)
   }
 
@@ -661,12 +661,12 @@ class TestPrettyWriter extends FunSuite with BeforeAndAfterEach {
     assert(expected == stringWriter.toString)
   }
 
-  test("Append(<<a>>, b)") {
+  test("Sequences!Append(<<a>>, b)") {
     val writer = new PrettyWriter(printWriter, 80)
     val expr = append(tuple(name("a")), name("b"))
     writer.write(expr)
     printWriter.flush()
-    val expected = """Append(<<a>>, b)""".stripMargin
+    val expected = """Sequences!Append(<<a>>, b)""".stripMargin
     assert(expected == stringWriter.toString)
   }