Yamma 0.0.11 Released (for easier theorem refactoring) Yamma now builds a (partial) theory, even if some proofs are not valid.
This is a feature that I wish mmj2 had, because it allows for easier change of theorems' signatures. Here's an example of how it works: in set.mm, ~ liminfgelimsupuz was written for sequences of reals. It had this (3rd) hyp |- ( ph -> F : Z --> RR ) But it was easy to amend its proof for extended reals. So you can go in set.mm and change its third hyp to |- ( ph -> F : Z --> RR* ) When Yamma reloads set.mm it will of course create Diagnostics for validation errors, and it will send you a final warning notification (for the whole theory being invalid). But it will load all the valid theorems, anyway (a valid subtheory) These are the Diagnostic errors you will get Theorem liminfgelimsupuz : $e hypothesis doesn't match stack entry. The current hypothesis on the stack is '|- ( ph -> F : Z --> RR* ) . The $e hyp with substitution is |- ( ph -> F : Z --> RR ) . Theorem climliminflimsup2 : Provable statement liminfgelimsupuz is in the theory, but its verification failed Theorem climliminflimsup3 : Provable statement liminfgelimsupuz is in the theory, but its verification failed Theorem climliminflimsup4 : Provable statement climliminflimsup2 is in the theory, but its verification failed Theorem climliminflimsup4 : Provable statement liminfgelimsupuz is in the theory, but its verification failed Theorem xlimliminflimsup : Provable statement climliminflimsup3 is in the theory, but its verification failed You see that you need to fix the proof of liminfgelimsupuz, and then the "immediately" dependent proofs of climliminflimsup2 , climliminflimsup3 and climliminflimsup4. xlimliminflimsup is fine because it does not depend immediately on liminfgelimsupuz, thus it does not need any change Now you can open the liminfgelimsupuz.mmp file and fix its proof, and create the .mmt file. Then use climliminflimsup2.mmp and climliminflimsup3.mmp to fix their proofs. Finally, use climliminflimsup4.mmp to fix its proof. The whole theory will then be valid. BR 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/1c2f8973-e23c-4639-a752-d20011e77e32n%40googlegroups.com.
