On Thu, 13 Jun 2019 00:45:47 +0800, Thierry Arnoux <[email protected]> wrote: > The table in the "convention" lists /some commonly used/ abbreviations. > > Shall we try to make it as exhaustive as possible so that it becomes a > /reference/, which can be used when one wants to find an existing > theorem, or name a new one?
If we made an exhaustive table then it'd have to include all the "df-..." entries. Ignoring mathboxes, that would require 779 definitions, only a few of which are there now (counted with grep 'df-.*$a' ,set.mm | wc -l). That's a pretty big table. I think the shorter table is easier to deal with, so I don't think we should eliminate the short table. If you want an exhaustive table, we could create a script to automatically generate an exhaustive table by combining the short table and the "df-... $a" definitions. We could run that once & edit by hand, or just rerun the script to keep generating the full table. An exhaustive table produced from a script is more likely to actually stay correct, once it's correct :-). --- 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/E1hb6qL-0005Yf-6C%40rmmprod07.runbox.
