I just opened a pull request for the second part of this: removing
unnecessary curly braces. See
https://github.com/metamath/set.mm/pull/2365. If anybody wants me to keep
my hands off of your mathbox, please let me know. That should mark the end
of the cleanup for now. Regards,
On Thursday, October 28, 2021 at 9:17:21 PM UTC-6 Jerry James wrote:
> I have been studying parts of set.mm that I want to understand better.
> While doing so, I have occasionally encountered unnecessary ${ $} pairs,
> and occasionally have seen $d statements for variables that do not appear
> in the theorems or proofs in that scope. Tonight I wrote a pair of scripts
> to detect these situations. It is a testament to the simplicity of the
> metamath grammar that I could write both in a single evening.
>
> Here is a 5-line awk script that identifies unnecessary braces:
> http://jamezone.org/pleasure/mathematics/metamath-braces
>
> This is the number of unnecessary brace pairs per mm file (skipping those
> with zero):
> - iset.mm: 51
> - nf.mm: 56
> - set.mm: 207
>
> For the second issue, I started writing awk code as well, but quickly came
> to the realization that the line-oriented nature of awk was not well suited
> to the task. Here is a python script that finds $d statements for
> variables that do not appear below the $d in the same scope:
> http://jamezone.org/pleasure/mathematics/metamath-dvs.py
>
> This is the number of variables it found per file (skipping those with
> zero):
> - hol.mm: 1
> - iset.mm: 1302
> - nf.mm: 390
> - set.mm: 6124
>
> Unnecessary braces and $d statements are not critical issues, of course.
> I offer these scripts to anyone who wants to declutter a metamath database.
>
> Regards,
> --
> Jerry James
> http://jamezone.org/
>
--
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/5b32d95c-6c2b-4a57-8814-52b1c27d3410n%40googlegroups.com.
