I think it is a good idea to couple the definition with the corresponding constant declaration. Since it is not allowed to have several definitions for the same constant (I made this experience some hous ago ;-)), I see no problems with it. But why not be more strict and combine the text areas (as far as I can remember they are mostly redundant), e.g.:
$( Text text. $) cfoo $a class foo $. df-foo $a |- foo = ( x e. bar |-> x ) $. Concerning the circular definitions: are there any meaningful cases, or even already examples in set.mm? Alexander -- 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/238c346b-90f8-477c-ac87-cfaae7e8d325%40googlegroups.com.
