FYI, I made some minor stylistic modifications to the el*v theorems in https://github.com/metamath/set.mm/pull/2472 ; you should use that as a base for modification to avoid conflicts.
On Fri, Feb 4, 2022 at 4:35 AM Mázsa Péter <[email protected]> wrote: > 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 > . > -- 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/CAFXXJSutsO728YztaxsAhYeuyR%2BVnRop2f4yzpWR7uTcF%2BtaYg%40mail.gmail.com.
