I noticed that there are many theorems with labels ending with "t", having a statement like "Closed form of ..." in their comments. For example ~trut: " A proposition is equivalent to it being implied by ` T. ` . Closed form of ~ trud . ...".
In the "conventions", it is written that theorems in closed form should not have a special suffix, or should have suffix "g" in special cases. A suffix "t" is not mentioned in the conventions. What does the "t" stand for? Should it be removed to follow the conventions, or should the conventions be enhanced? In which cases a suffix "t" should be used, and in which cases no special suffix? -- 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/716aedcb-5c0c-4e58-98eb-bcc87c3d0c91n%40googlegroups.com.
