On 2/3/22, 'Alexander van der Vekens' via Metamath wrote: > * I agree with Mario that stars should not be allowed after or within > labels, at least if they are used with ~ to auto-link them.
Of course I agree as well. 4 options remained: ( ~ elv , and the theorems beginning with ` el2v ` or ` el3v ` ) ( ~ elv , and the theorems beginning with el2v or el3v ) ( ~ elv , ` el2v* ` and ` el3v* ` theorems) ( ~ elv , el2v* and el3v* theorems) Perhaps the first is the best, I'll make experiments. On 2/3/22, 'Alexander van der Vekens' via Metamath wrote: > Wouldn't $p ` |- ( A e. V -> ` be sufficient? On 2/3/22, Mario Carneiro <[email protected]> wrote: > For the purpose of > this particular comment I think it suffices to just have ` |- A e. _V ` in > the description. I agree here as well, I will try this: Inference forms (with ` |- A e. _V ` ) of the general theorems (with ` |- ( A e. V -> ` ) may be superfluous. On 2/3/22, 'Alexander van der Vekens' via Metamath wrote: > * quoted strings longer than a line can be split up. See, for example, ~ > numclwwlk7. I think this is a sufficiently good solution. On 2/3/22, Mario Carneiro <[email protected]> wrote: > As mentioned, the fix is to split the math string by closing it on the > first line and reopening it on the second line. The renderer will combine > the strings. This is perfect! I didn't know about this option. Thank you. Peter -- 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/CAJJTU5ppfdp40ZM9suURAKNc%2BDNqJnZubhzVsFudGQwdTa1uaw%40mail.gmail.com.
