Hello, I try to understand MM1 tacticts, but they seem so intricated to me when i look at code (peano.mm1 for example), i wonder what tools people use to elaborate proofs with tactics, because i guess they are not entirely man-made. I used the vscode plugin, but it did'nt really help to understand the tactics because of the lisp-like syntax/keywords.
-- 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/CAC0Jddi-jHk%3DfOm%3DEK59Vtedj_Wne778kBFeSvPNM%2B2i8r5bZQ%40mail.gmail.com.
