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/CAFXXJSsJp7s_Bs5U-XFsxfGu1fBzSc6kjQAtt0GbKYrn7dDT4w%40mail.gmail.com.
