Greetings, Metamath-ers, As a hobbyist of set theory, logic, and the programing language Julia, I've been refactoring the Metamath Julia implementation to provide better interactive usefulness (in addition to using an old version of Julia, the previous incarnation could only load in .mm files and verify them). This has been a learning experience about the nuances in the details of the Metamath specification (i.e. the pdf file that will be printed soon).
I've run into a roadblock where I can't find anywhere in the specification (section 4.1 of metamath.pdf) where dummy variables are to be treated as distinct; there's no mention of it in 4.1.4. In the frames section (4.2.4, page 131), I see a definition of "optional disjoint-variable restriction", but I don't see anywhere that actually says to treat them as disjoint. I also see the "Dummy variables <list> are mutually distinct and distinct from all other variables" comment on the webpages for the set.mm theorems. Am I missing something? -- 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/d4ce66a2-e2aa-4791-b10e-f39d0dff7f3e%40googlegroups.com.
