> You can do that, but ideally this would be done as a change to the exporter, so that the theorems themselves can be stated using the notation, and also so that it stays up to date with set.mm. So the exporter will have to identify whether a notation is prefix or infix or a general notation, and there will be compromises needed on some set.mm notations that are mm0-ambiguous, like wa `( ph /\ ps )` and w3a `( ph /\ ps /\ th )`. In MM0 every notation has to start with a unique token.
Ok, this sounds good to me. I will probably need one example to see how it works, but after that I should be able to figure out how to carry on with the notation. For w3a, one could disambiguate using a slightly different symbol, not already present in set.mm, like `( ph /\. ps /\. th )`. A problem with this approach is that someone might add a definition in set.mm with the `/\.` symbol in the future and then the translation would break because of a conflict between tokens. One could avoid it by using special hidden symbols, but this is probably against the transparency philosophy of MM0, so I'm sure there are plenty of reasons why this is bad. Another possibility could be to tell the exporter to automatically replace `(w3a ph ps ch)` with `(wa (wa ph ps) ch)` everywhere before introducing the notation. The original set.mm would not be preserved, but since the theorem being edited in MM1 would verify anyway in the original set.mm, I think it would not be a problem. There are also df-op `<. A , B >.` and df-ot `<. A , B , C >.` that have the same obstacle. Dropping df-ot might be ok, but this approach becomes problematic for definitions like df-s1, df-s2, df-s3, df-s4, etc.. which really make statements about words shorter. I think dropping those might not be acceptable. I guess the easy ones to automate are class constants. Looking at peano.mm0, I notice that (all?) constants are defined as prefix operators with maximum precedence (e.g. def d1: nat = $suc 0$; prefix d1: $1$ prec max;). If that's the case, then it seems feasible to make a complete manual list of problematic definitions and decide how to handle them. The vast majority of set.mm definitions are just class symbols all different between each other. -- 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/cb053781-1156-4323-9c41-40c44771684en%40googlegroups.com.
