search

metamath / set.mm

Metamath source file for logic and set theory
Creative Commons Zero v1.0 Universal
238 stars 87 forks source link

0a = 0 (mulcom pr 10) #4068

Closed icecream17 closed 2 weeks ago

icecream17 commented 2 weeks ago

mathbox

comments:

I'm glad this is possible, though it's quite involved

In the middle of proving 0tie0 I messed up. mmj2 cant edit incomplete metamath.exe proofs, but the show new /lemmon /ren /no_repeat command was similar enough to mmj2's syntax that I could get it to work with some editing, copying, and pasting. At minimum, this suggests it would be relatively easy to make a script for the use case of editing incomplete metamath.exe proofs in mmj2 (and also yamma).

Also I suspect that windows wraps at 79 columns instead of 80 because in windows, metamath.exe uses CRLF line endings instead of LF line endings. (I did git diff and the different line endings resulted in a failed memory allocation. Luckily my computer only lagged at 100% disk for a minute)

wlammen commented 2 weeks ago

It should be part of the specification, what the kind of line ending is, to avoid any hassle with different operating system. If metamath(.exe) is generous enough to accept all kinds of endings, (CR on Mac Classic, CR LF on Windows, LF on Linux) then the usable space for text before this ending should stay fixed at 80 characters.