ok, I'll fix this after #2472 merge On 2/4/22, Mario Carneiro <[email protected]> wrote: > 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. >
-- 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/CAJJTU5rjfouTa4z6jv4BA81gnabkfVDz_8HGNCUua_x_JTugbw%40mail.gmail.com.
