Oh, I missed the recent #76, which does not have the marking "This is
Metamath 100 proof #76" in its comment yet ...
On Monday, December 30, 2019 at 9:09:31 AM UTC+1, Alexander van der Vekens
wrote:
>
> Hi David,
> I fully agree with you - I also suggested to move all theorems of the
> mm100 list which are still in mathboxes into the main part of set.mm a
> long time ago. If I counted correctly, there are still 10 such theorems in
> mathboxes: #9, #30, #45, #61, #73 ("part of"?), #77, #83, #87, #88 ("part
> of"?), #90. I would propose to creare an issue in GitHub for each of them
> (as I have done for #49, see issue #1333, which will be finished by my
> recent PR #1361), so that we can track the progress of moving them to the
> main part. I would start working on the issue for #83 next year ;-).
>
> Alexander
>
> On Monday, December 16, 2019 at 4:41:23 PM UTC+1, David A. Wheeler wrote:
>>
>> As I recently posted, I believe that all "Metamath 100" results (and thus
>> all they depend on)
>> should eventually move into the main body. After all, all Metamath 100
>> results are
>> results that at least some others believe are important. I suspect the
>> folks who already produced metamath 100 results would be the best situated
>> for proposing where things go.
>>
>> So: if you produced a metamath 100 result, but it's currently not in the
>> main body, I would love to see your proposals to start moving their
>> dependencies and the result itself into the main body. If there are many
>> parts, I expect that mini case it would be easier to do it slowly in pieces.
>>
>> There is no rush. That said, I think it's important to keep working on
>> getting more things moved from mathboxes
>> into the main body. Tools like mmj2 only consider items in the main body
>> for
>> many automated steps, and in any case I think it's far more sensible to
>> readers if major results are properly organized in the main body.
>>
>> --- David A.Wheeler
>
>
--
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/1bcc52fb-c945-404d-aa29-027374f98cce%40googlegroups.com.
