On Friday, June 14, 2019 at 9:56:57 AM UTC-4, ookami wrote: > > Am Freitag, 14. Juni 2019 14:55:10 UTC+2 schrieb Mario Carneiro: > > [..] If I see a constant, how far forward do I need to scan to find out >> whether this is actually a definition? [..] >> > > My mathbox will not be affected by your proposed change. I am unable to > judge whether this change has unwanted side effects in the future, > preventing something like your depicted circular references. However, if > you aim at coupling the constant definition and its usage in a definition > more tightly, why not make this explicit by extending the syntax of a > constant definition like this: > > $( Text text. (Referenced in definition df-foo.) $) > cfoo $a class foo $. >
If the syntax axiom is placed immediately before the definition, which I think is what Mario proposed, this tag seems a little bit redundant since it is easy to check either by a human or a program. > > This will not break current parsers, or editors sensitive to Metamath > grammar. The style is already used with New usage.. and Proof > modification.. tags, so it does not introduce anything new to Metamath. > > What about implicit definitions like df-bi, but involving two constants in > two defining expressions? Do you really want to rule out this? > The four definitions df-bi, df-clab, df-cleq, and df-clel are excluded from the current definition check. Any new software will have to treat these 4 as special cases, for example by treating them as additional axioms. Hopefully these 4 are the only ones that will ever need special treatment. Norm -- 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/ed078cbc-fca0-4128-ba78-ddfd06e3c341%40googlegroups.com.
