Hi and welcome, Corbin. * The proof assistant is alright. I'm able to integrate it with my editor somewhat, and to prove one or two proofs at a time, slowly.
did you try mmj2? I alt + tab between it and an external (more powerful, general purpose) editor, just to search / replace strings, and (once you get used to it) it's not bad at all. A couple of keyboard shortcuts to save/reload your current .mmp file and you can focus on the proof. I now feel like I'm the real bottleneck, not the IDE (and I'm confident, sooner or later, the community will further improve mmj2). Glauco -- 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/8b82e2e2-6c52-4e42-bc60-5481da9431f8%40googlegroups.com.
