> No worms, just more support for a widely-used symbology. > The problem is that it's not obvious if A and E have some sort of correspondence, > but it's obvious that A and A' are intended to have some sort of correspondence.
The problem is that this kind of symbology arises in other fields as well. I personally, for example, find relations difficult to read in Metamath, especially when they are chained. One can easily argue along your lines that a different font for differentl set types improves readability - and I agree, it would! Or enclosing subexpressions in parentheses could be relaxed by prioritizing operators. And, and, and... . Your idea is just one out of a plethora of typographical aids to point out the semantics of formulas. Thats why I speak of a can of worms. > I have no idea how to implement a translator that could figure out, > ahead of time, that A and E have a correspondence in a particular theorem. > Nor should we do so, because that would create an undesirable distance > between the actual set.mm proof and its display. There is no simple solution to this problem. My first idea is that a processor evaluates a tag like comment with hints on how to display otherwise difficult to read math expressions. This has to be written from scratch. Improving readability is just a task completely different from proofs, and can/should be solved separately. Wolf -- 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/d328a25d-e65e-41ad-a7dc-af4d1e820bfen%40googlegroups.com.
