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 $. 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 Wolf -- 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/174a048b-4d46-4336-b0bb-94185fee4d70%40googlegroups.com.
