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

Re: [tlaplus] Unicode

   So all the complicated logic is in program 1

Indeed.  You will, of course, write a specification of the two translations for others to examine.  I think you will find it to be an interesting exercise.  The Toolbox's Decompose Proof command has to solve the problem of maintaining indentation while expanding definitions in a proof step.  It works right most of the time, but it's not perfect.  Program 1 will have to be perfect if people are to trust it.