[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Unicode

On Tuesday, March 29, 2016 at 5:14:56 PM UTC+3, Stephan Merz wrote:

That's a bit over-simplifying. For example, you could have

 x \in { s \in S : /\ \/ A(s)
                      \/ B(s)
                   /\ C(s) }

If you replace "\in" in the first line by the corresponding Unicode symbol, you break indentation.

That's not a problem because the text would be replaced as you type (i.e once you hit space after \in you get it replaced with ∈ etc.), so you'd really be typing this:

  x ∈ { s ∈ S : ∧  A(s)
                  ∨ B(s)
                ∧ C(s) }

which is aligned in unicode, and then program 1 would convert it to your ASCII version, fixing indentation to yield a version aligned in ASCII. So all the complicated logic is in program 1.