On 2/3/22, Mario Carneiro <[email protected]> wrote:
> On Thu, Feb 3, 2022 at 2:45 AM Mázsa Péter <[email protected]> wrote:
> 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).
The function of it is cross referencing by searchability. If you are
able to put searchable strings into the notes of theorems, they may be
not cross-references in html-way, but they are cross-references in a
way that you can search them in set.mm locally.
2 examples:
>> Inference forms (with ` $e |- A e. _V $. ` ) of the general theorems
>> (with ` $p |- ( A e. V -> ` ) may be superfluous.
You search for $e |- A e. _V $. locally and you see that these el*v*
theorems refer to 395 theorems in set.mm containing $e |- A e. _V $. .
Or:
$( Two ways of saying that two classes are disjoint (when ` C = (/) ` :
` ( ( A i^i B ) = (/) <-> ( B i^i A ) = (/) ) ` ). (Contributed by Peter
Mazsa, 22-Mar-2017.) $)
ineqcom $p |- ( ( A i^i B ) = C <-> ( B i^i A ) = C ) $=
( cin incom eqeq1i ) ABDBADCABEF $.
means that when you search for ( A i^i B ) = (/) in set.mm you will
find the more general ineqcom (rendered perfectly az
http://us.metamath.org/mpeuni/ineqcom.html ). The problem is that if
you put too much characters between ` and ` , the /rewrap feature is
not able to rewrapping it: how should I quote longer strings? And: if
you write e.g. ` u ( `' _E |` A ) x ` in the notes of a theorem, it is
not allowed by verify markup, because the second ` is interpreded as
the closing ` instead of the third one.
So what I ideally want is:
*a general method
*for quoting
*arbitrary strings
*arbitrary lenght
*for searchability in set.mm
*showing in html version
*verifying markup
--
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/CAJJTU5oxJQQOo88VzTQOqKNy5Q1AHrKX4XpC%3DRH1grm0p8rqkw%40mail.gmail.com.
