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/ab5d3628-1e97-49b1-867c-e9ce55dd0a74%40googlegroups.com.
