> > > How about adding some weasel words to the affected definitions? Such as: > "This definition is technically an axiom, in that it does not satisfy the > requirements for the definition checker. The proof of conservativity > requires external justification that is beyond the scope of the set.mm > axiomatization." >
I propose to put expressly and extensively all the checks made by mmj2 in a page on the site. I believe (?) that there is no such thing. And to add details on why these checks do not affect the power of metamath (as for the prohibition of functions that call themselves.) -- 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/96b65030-0c0e-4687-be74-a4650b70546a%40googlegroups.com.
