[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.