This actually made me curious because this should have been caught by the existing VERIFY MARKUP check already, yet http://us.metamath.org/mpeuni/elv.html has already made it to the develop branch and the web site. It looks like VERIFY MARKUP has been disabled in CI? @David what's going on here? Looks like it's been like this since december: https://github.com/metamath/set.mm/commit/b6d91985163285cb27ecfcc46c31e4e4791dc2ab .
Mario On Thu, Feb 3, 2022 at 3:07 AM Mario Carneiro <[email protected]> wrote: > > > On Thu, Feb 3, 2022 at 2:45 AM Mázsa Péter <[email protected]> wrote: > >> Hi Mario, >> >> >> I have 3 questions: >> >> 1. You see >> ( ~ elv , ~ el2v and ~ el3v theorems) >> here: http://us2.metamath.org/mpeuni/elv.html >> In /develop, you find >> ( ~ elv , ~ el2v* and ~ el3v* theorems) >> > > I see this in set.mm: > > ${ > elv.1 $e |- ( x e. _V -> ph ) $. > $( New way ( ~ elv , ~ el2v theorems and ~ el3v theorems) to shorten > some > proofs. Inference forms (with ` $e |- A e. _V $. ` ) of the general > theorems (with ` $p |- ( A e. V -> ` ) may be superfluous. > (Contributed > by Peter Mazsa, 13-Oct-2018.) $) > elv $p |- ph $= > ( cv cvv wcel vex ax-mp ) BDEFABGCH $. > $} > > I didn't find this in my local copy, I guess it's a new addition. If I had > it would have shown up in my markup check because $e and $p are not tokens. > > Is it possible to refer to a set of theorems with one string? I mean, >> you understand that ~ el3v* means all theorems beginning with el3v >> (i.e. ~ el3v ~ el3v1 ~ el3v2 ~ el3v3 ~ el3v12 ~ el3v13 and ~ el3v23 ), >> but can you express this in a way that shows ( ~ elv , ~ el2v* and ~ >> el3v* theorems) here http://us2.metamath.org/mpeuni/elv.html as well? >> Or should I write this: ( ~ elv , and the theorems beginning with ` >> el2v ` or ` el3v ` ) ? (Or is it solved already just didn't show up at >> us2.metamat.org yet?) >> > > I would not recommend using stars after or within labels, at least if you > use ~ to auto-link them. What do you expect to happen? It's an HTML link, > it can't link to a whole collection of things even if it could determine > what collection you are talking about. Alternatives include linking to all > of them, linking to one or two "representative" examples with some text to > indicate that there is more, or just using the glob notation and linking > nothing. > > 2. You see >> Inference forms (with ) of the general theorems (with ) may be >> superfluous. >> here: http://us2.metamath.org/mpeuni/elv.html >> In /develop, you find >> Inference forms (with ` $e |- A e. _V $. ` ) of the general theorems >> (with ` $p |- ( A e. V -> ` ) may be superfluous. >> How should I express what I want? >> > > What *do* you want? You can just leave off the ticks and they will be > printed in regular text, or you can use quotes (and they will still be > printed in regular text), or you can use <HTML><PRE></PRE></HTML> to render > them in monospace font. > > >> 3. Reference to the ` $e |- A e. _V $. ` stings in set.mm (cf. above) >> are verified by the verify markup feature. Sometimes, in the notes >> parts of other theorems, I want to refer to longer strings in set.mm , >> but verify markup doesn't allow it. Is it a way to do it? >> > > I don't understand the question. Math strings allow you to render > metamath token strings the same way as they would appear normally in > proofs. They don't do any cross referencing. Label references can be used > for cross referencing, and they only link to theorems, not subsections or > other things like that, although you can use <HTML> to write arbitrary > markup if you really want (although I think this was a bad idea and I would > like to decrease use of <HTML> in favor of more structured markup). > > Mario > -- 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/CAFXXJSvrO%2BB15uKq2O6cCNJg_1x3YpkCkLynf4vrvyM5fYLRNQ%40mail.gmail.com.
