On Monday, January 6, 2020 at 4:59:25 PM UTC+1, Benoit wrote:
>
> On Monday, January 6, 2020 at 7:03:23 AM UTC+1, Mario Carneiro wrote:
>>
>> I wish we would stop using the description comment for metadata like
>> this. This is the sort of thing that makes markup parsing the rats' nest
>> that it is. Just have a separate comment, with a sane computer-readable
>> grammar. (It should also contain the "contributed by" and "usage
>> discouraged" information, which are also metadata. Using english words just
>> fools people into thinking there is no strict grammar.)
>>
>
> I think this would go in the good direction. I can make a loose analogy
> with another math hobby I contributed to: Neil Sloane's Online Encyclopedia
> of Integer Sequences (OEIS). Every set.mm proof has its own webpage (in
> the Metamath Proof Explorer), which in some respects has similarities with
> each sequence of the OEIS and its webpage (e.g., each has a name/label, a
> comment, an author, a date, etc.). The format is explained at
> http://oeis.org/eishelp2.html with a link to the description of the
> "internal format" (for an example, see e.g. http://oeis.org/A3).
>
I also like the idea to remove the metadata from the comments and to
provide them separately. Another analogy could be taken from Java - the
annotations. For ~rucALT, for example, this could be as follows:
$( $j @acronym r+uc+ALT
@name real numbers are uncountable
@author NM
@since 13-Oct-2004
@revised 13-May-2013 Mario Carneiro
@shortened 13-Sep-2020 AV
@discouraged usage proof_modification
@references ~ ruc ~ rpnnen
$)
$( This proof is a simple corollary of ~ rpnnen , which determines the
exact cardinality of the reals. For an alternate proof discussed at
~ http://us.metamath.org/mpeuni/mmcomplex.html#uncountable ,
see ~ ruc . $)
rucALT $p |- NN ~< RR $=
@acronym, @author, @since would be mandatory, the rest optional. @revised,
@shortened could occur more than once. The order may not be fixed (to be
discussed).
To put the annotations into separate lines should not be mandatory, so so
following would also be possible (but not recommended, in my opinion):
$( $j @acronym ruc+ALT@name real numbers are uncountable
@author NM @since 13-Oct-2004 @revised 13-May-2013
Mario Carneiro @shortened 13-Sep-2020 AV
@discouraged usage proof_modification @reference ~ ruc
$)
$( This proof is a simple corollary of ~ rpnnen , which determines the
exact cardinality of the reals. For an alternate proof discussed at
~ http://us.metamath.org/mpeuni/mmcomplex.html#uncountable ,
see ~ ruc . $)
rucALT $p |- NN ~< RR $=
Currently, the comment is as follows (does not have a "Proof shortened"
parenthetical):
$( Alternate proof of ~ ruc . This proof is a simple corollary of ~
rpnnen ,
which determines the exact cardinality of the reals. For an alternate
proof discussed at
~ http://us.metamath.org/mpeuni/mmcomplex.html#uncountable , see ~ ruc
.
(Contributed by NM, 13-Oct-2004.) (Revised by Mario Carneiro,
13-May-2013.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
rucALT $p |- NN ~< RR $=
We could, however, start with providing acronyms and/or names (which was
the original intention of this topic) in such a way, but prepared for a
future extension.
Alexander
--
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/4a14768e-bf53-4884-af4d-e64f716cedea%40googlegroups.com.
