> This is not a legal definition, this is mutual recursion which is not > allowed. If you tried this in set.mm today you would get an error because > mmj2 would not allow df-log to reference mulc. You would be forced to have > an intermediate definition for the finite multiplication operation, even if > you never use it / immediately eliminate it after the trio of definitions. >
Of course! I had overlooked that. I'll be using only the clause of the "if" that does not involve the future definition, but that's in the object language, and metamath can't know that. So I'll need temporary definitions, like what is currently done in the construction of the number systems. The question is then to which extent this is acceptable... I'll come back when I have something more concrete to propose. > While I am not proposing this as part of a rigorously checked rule, I'm > fine if we do this. But unlike term/definition pairs, which have to come in > pairs (because any new constant requires a definition), there is no one to > one relationship between $c constants and new syntax axioms. $c > declarations are more about presentation, the token alphabet from which the > CFG is defined. A new term can reuse old constants, or introduce new ones, > so there might be no new $c's with a term (for example df-mpt2), or there > might be more than one (for example df-itg). Additionally, metamath allows > $c declarations to be bundled into one declaration, which makes it more > convenient to declare them all in a single block. > You're right, there is no bijection, so the rule could be: $c the new symbols used in csmurf $. (here, $c smurf }} $. ) csmurf $a class smurf [ A }} $. df-smurf $a |- smurf [ A }} = ... $. As for the reuse of symbols, like in df-mpt2, would it be good practice to require at least one symbol unique to each definition? It could be useful for searching. E.g. how do you single out occurrences of functions of two variables with the "MM> SEARCH" command (or even searching with ctrl+F in a text editor)? I guess this is doable in mmj2 with regular expressions? I've been a bit extreme in not overloading symbols, and defined couples of classes as (| A ,, B |) (see bj-c2uple), although the unicode symbol for ",," is "," so that the couple looks more normal on the webpage. Benoit -- 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/ebd492bd-49c3-4ced-99e8-eb4c1b599915%40googlegroups.com.
