I have made some progress on trying to write my first proof but I am running up against several annoyances that would make many prospective users quit in frustration:
1. The java version of mmj2 that I downloaded keeps crashing or freezing (no response to cancel). 2. There is no autosave so every time it crashes, I lose my work. 3. It is not browser based so it does not work on my tablet. This limits the time I can devote to it. 4. The search feature is cumbersome. 4a. There are 4 windows (cmd, editor, search box, search results) to toggle between. 4b. The search window is too crowded with features that I don't know how to use. 4c. No clear and easy way to copy/paste text from the result window. 5. Searching for ( X + Y ) does not return ( A + B ) 5a. I am sure a regular expression could fix that but I could not find examples and I am tired of crashes. 5b. Regular expressions are hard to use when looking for a pattern with nested parentheses. 6. I do not know whether I should look for "( A x. B ) = 0" or for "A x. B = 0" and the search seems to care. 7. Searching for ==> or for && to find implications returns nothing. 8. I could not find something as simple as: "|- -. ps && |- ( ph \/ ps ) ==> |- ph" 8a. Maybe it does not exist in set.mm but I can't tell if it does and that is frustrating. 9. I want to use |- A e. CC ==> |- ( ( 2 x. A = 0 ) <-> A = 0 ) 9a. I do not know if it already exists or if I need to prove it myself. 9b. If I have to prove it myself, I'd rather prove: |- A e. CC && |- B e. CC && |- B =/= 0 ==> |- ( ( B x. A = 0 ) <-> A = 0 ) 9c. Having it in this form will make my proof shorter but I see a preferece for deduction form in set.mm 9d. Do I need extra proof steps to go back and forth between: "|- 2 =/= 0", "|- -. ( 2 = 0 )" and "|- -. 2 = 0" ? 10. I understand the advantages of deduction form and the desire for shorter proofs but ... 10a. Searching for two possible versions of a theorem is frustrating 10b. Having to write two versions, name them and justify them is daunting. I am not ready to give up, but any help or suggestions on how to use my time more effectively will be appreciated. Noam. -- 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/c64450bd-2059-4a71-b66d-3d99ad3f307f%40googlegroups.com.
