Hello metamath community, I'm still working on my upcoming mmj2 inspired proof assistant called mmt1 and I am now getting around to implementing work variables. This got me thinking about the design of work variables in mmj2 and I wanted to share some thoughts with you.
First, what happens when a database has a symbol declared that is the same as a work variable (e.g. &W1)? Does the symbol become unusable or will mmj2 stop treating it like a work variable? Second, what happens when multiple typecodes start with the same letter? Will they have different looking work variables? Third, what happens when a typecode starts with a number or a non-letter symbol? This doesn't necessarily break the design, but it could make for some weird looking work variables. Note that the questions above are more or less rhetorical and if you don't happen to know the answers I wouldn't recommend looking for them, as that could take some time. What I am more interested in is what you guys think a proof assistant SHOULD do. To me it almost seems that you would have to completely redesign the syntax of work variables to fix these issues. One way would be to change the & to a $, so that you can't define symbols that look like work variables. Then you could change the capital first letter of the typecode to allowing any variable with that typecode. This then leads to another problem: What if a variable ends in a number? To solve this you could move the dollar between the variable and the work variable number. This would then give you work variables like: ph$1, x$2, A$3. This leads me to my main set of questions: Would you prefer this more universal syntax over the old one? Are the problems I described so rare that it all doesn't really matter. What should the proof assistant do if a database nevertheless has these problems? Just reject it? Thanks for any answers in advance! Marlo Bruder -- 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 visit https://groups.google.com/d/msgid/metamath/4f50b1ee-6911-4397-b52c-752b4a7e0745n%40googlegroups.com.
