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

Re: [tlaplus] Unicode

On Tuesday, March 29, 2016 at 6:25:26 PM UTC+3, Leslie Lamport wrote:

The Toolbox's Decompose Proof command has to solve the problem of maintaining indentation while expanding definitions in a proof step.

I don't know how the toolbox communicates with TLAPS, but assuming this decomposition work is done in the toolbox, then isn't it just a matter of doing it either entirely in unicode or entirely in ASCII? Program 1 can then work on complete files only (both input and output). Or did you just mention this as an example showing that maintaining indentation can be tricky?