On Fri, Dec 5, 2025 at 2:22 AM Gino Giotto <[email protected]> wrote:
> > The thing I like metamath.exe isn't automation, but rather that it's fast to create proofs once you get confident with the commands. Since it's a CLI, you avoid many mouse movements, and so far I've preferred this design over editor-based proof assistants. Which reminds me, I started learning Vim Motions to avoid mouse movements, and would like to persist but haven't got around to it. In terms of writing proofs, that would probably then be done in Visual Studio Code with the Yamma, and Vim (vscodevim, 8 million downloads) extensions installed and enabled. The advantages of this is that I'd be learning a way to avoid mouse movements when editing any kind of text file, not just for proof writing activities, and I'd be able to start my proofs at the beginning or middle. The disadvantage is that you're already very comfortable with metamath.exe as a proof assistant, and I wouldn't contemplate a change either under those circumstances! :-) I don't really feel any particular discomfort when I'm crashing around with a mouse and keyboard, but I've made a live coding video <https://youtu.be/TcUvUWJjVvA?si=e-je1kHr5kdPvj0f> or two <https://youtu.be/3vR9nLjSZ9w?si=y7pb8mNPgkezrpvy>, and re-watching myself crashing around *is* rather painful ;-) Best regards, Antony -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/CAJ48g%2BCLKtJb4FGSm0nTwFryuJSQfzsSjFKCgeKDDfw4X518jg%40mail.gmail.com.
