|
|
|
|
|
|
by qznc
4158 days ago
|
|
|
After reading that, I think structured proofs should be written with an outliner [0] interface, where you can actually expand and collapse the hierarchy. Lamport also knows this. He repeatedly mentions it as "hypertext". However, he seems to be locked into LaTeX [1] and pdf generation. [0] https://en.wikipedia.org/wiki/Outliner [1] Not really surprising. Lamport invented LaTeX. |
|
|