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.