Comments on doc/lang.md

[lasarojc]

Thanks for the extensive documentation. Here goes some comments/questions on this specific file and TNT in general from my first interactions.

1. What is the cost of not declaring a definition as pure? Is it in performance when running Apalache?

2. Would it be possible to support if p then e1 else e2 instead of/in addition to if (p) e1 else e2? IMHO it is much more eye pleasing, specially if the condition spans multiple lines (I can never find a pleasing way to indent the parenthesis).

3. If we do not expect people to be coming to TNT from a TLA+ background, why not support CASE?

4. With respect to discriminated unions

   1. Use the same syntax for members of the union as for records, that is name_1 instead of <ident> or the other way around.
   2. The documentation seems to imply that a type with name <tag value>_TYPE is created for me, but experimenting with REPL indicated otherwise (val x = { tag: "Cat", name: "Ours", year: 2019 } followed by var xt : CAT_TYPE)
   3. Can we filter elements of a set based on fields other than tag? I tried Entries.filter(e => e.year == 2019) and it worked but with a warning.
   4. Can we match fields other than tag? If so, I'd consider matching on tag to explicitly require the field name.
   5. In the REPL, how to type multiline match expressions? I couldn't execute the match example.

5. Regarding lists, replaceAt(l, start, end) should be replaceAt(l, I, e)

6. Regarding Then

   • “The semantics of this operator is as follows. When A.then(B) is applied to a state s_1, the operator computes a next state s_2 of s_1 by applying action A, if such a state exists.”
   • Where is s1 defined? Isn’t A the state here? Maybe it should be written as (A).then(B) and in this case A initializes the state s1 and s_2 is computed by applying B?

7. Regarding Set, a common operation is to add one element e to a set s . In TLA+ it was s \cup {e} (which looks clean on a pretty print), but in TNT it is longer s.union(Set(e)). Would an add make sense here (s.add(e))?