Am Freitag, 14. Juni 2019 19:30:43 UTC+2 schrieb Norman Megill: > > 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? [..] >>> >> >> [..] 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. >
Apparently I was not clear enough. By using a tag (or other kind of reference) the positioning of entries remains unrestricted, open for any future development. I interpreted Mario's foo/bar example in a way that he himself was in doubt whether forcing constant and definition into consequtive entries might cause harm in the future. Wolf > >> [..] >> 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/396cb748-dacc-4899-ba39-ed58624c32c0%40googlegroups.com.
