Hi all. I'm in the process of writing my own Metamath database. To start, it's basically a refactoring of the logic portion of the set.mm database but with my own numbered naming system for theorems in order to correspond with a pdf book that explains things informally but in more detail. Anyways I will share more later if anyone is interested.
My main issue is when writing proofs I sometimes wish to use a specific theorem for the sake of clarity, but the proof assistant will automatically complete the proof with a different theorem. This happens because proof assistant seems to always choose the earliest theorem, while, for the sake of presentation, I might prefer to use a later version that accomplishes the same thing. Sometimes I will restate earlier theorems just to group them ( for instance, restating all natural deduction rules in one place ). In any case, this means I sometimes need to clear the justification field and carefully type in the name of the theorem I wish to use. This process would be faster if there was a feature where instead of using the proof assistant I could simply type a search query and pick from a list. -- 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/f12aa384-539d-4ff3-9fc3-51257ed08e31n%40googlegroups.com.
