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/ff2c85a4-8ddd-4b6b-b27a-bf5867addf81n%40googlegroups.com.
