Awesome, thanks for the help :) I agree with you Benoit that exp is a nice word for Euler's constant and related function so I've relabeled the theorem as itgpowd (I think d is consistent as it is a deduction theorem). I think it would be good to change dvexp <http://us.metamath.org/mpegif/dvexp.html> etc too but I don't think I can do that. I removed the non-deduction version as I agree it is not so useful.
When you say to use " MM-PA> minimize * /no *" when should I use that? I do proofs in mmj2, do I need to load them in metamath.exe somehow? When following the list of instructions: https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md <https://www.google.com/url?q=https%3A%2F%2Fgithub.com%2Fmetamath%2Fset.mm%2Fblob%2Fdevelop%2FCONTRIBUTING.md&sa=D&sntz=1&usg=AFQjCNE1OXgquSEjXLP2JjG7C0sp1frjMw> I get this error, not sure what is happening, maybe it is not important to verify markup MM> verify markup */file_skip/top_date_skip ^^^^^^^^^^^^^ ?Expected DATE_SKIP, FILE_SKIP, or VERBOSE. MM> It is happy if I use: MM> verify markup */file_skip/date_skip How long is the character line in set.mm, it looks like 79 characters long, is that right? Seems like an unusual choice for the length. I understand about high in the tree I think, e.g in ((A = B) -> (C = (D + F)) the -> is high and the D+F is low. A more general philosophical question: is there some thing about how "it must be deduction form all the way down" in the sense that if I do some proof A in non-deduction form and then B relies on A then B cannot be in deduction form. Does this mean it's important to build the whole tree in deduction form? I have the proofs arearect and areaquad and I guess I would need to go back and put them in deduction form, which maybe isn't so hard. -- 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/8ba1977b-9fce-4abb-bd64-c26fc80a4e6c%40googlegroups.com.
