Hi Andrew,
I don't think hoping/dreaming for better tools is against The Metamath Way or anything.
Completely agree!
Following a discussion in this group a while ago, I've started to work on a VS Code extension for Metamath, you can find it here: https://github.com/tirix/metamath-vspa. It currently provides features such as syntax highlighting, "go to definition", "search references", "show proof", etc. Glauco has been helping with testing. I would like to add other functionalities so that it can match the Eclipse plugin <https://www.youtube.com/watch?v=BsEyW3vBcsE> I've been using to do formalization, hopefully also including some proof assistant functionality. I also think one could build it up to a Metamath proof assistant using tactics, but that's a longer term goal. BR, _ Thierry -- 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 on the web visit https://groups.google.com/d/msgid/metamath/40a1fa4b-be70-5107-159c-f1b0e35eaae2%40gmx.net.
