I suppose we should document "t" as meaning closed form (although it is far less common than no suffix). We perhaps could get rid of "t" with a modest amount of renaming (as far as I could tell from "show label *t"), although when I look at something like all the *19.21* theorems, finding good names for everything might be a touch complicated.
On April 11, 2022 4:29:08 AM PDT, 'Alexander van der Vekens' via Metamath <[email protected]> wrote: >There is a post of Norm >(https://groups.google.com/g/metamath/c/JWm26Y9qD-g/m/nhe6f87bBQAJ) withn >the following statement: > >"Suffixes "i", "d", "t" mean inference, deduction, and closed theorem >versions as usual." > >Unfortunately, there is no hint what "as usual" means/refers to. > >On Monday, April 11, 2022 at 1:17:27 PM UTC+2 Alexander van der Vekens >wrote: > >> 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/102ed4fd-654c-4acb-9633-34f194d7e96dn%40googlegroups.com. -- 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/6468E5E1-68E9-48CF-B220-81C16678CE8C%40panix.com.
