On Sun, 12 Jul 2020 14:24:34 -0700 (PDT), "'ookami' via Metamath" <[email protected]> wrote: > (1) How do you expect this to be clearly distinctive from df-fv?
The usual way, by their rotation. df-fv uses backquote, that is: ` Primes in set.mm currently use straight quote, that is: ' Many programming languages already depend on people being able to see the difference. If it's desired we could make prime markings more distinctive in Unicode by using U+2032 (HTML Entity ′ aka ′ aka ′). Here's a compare & contrast: ASCII: ( F ` A' ) Unicode: ( F ` A′ ) > (2) There > are numerous write styles in use for all kind of mathematical classes, e.g. > I've seen German Fraktur for topological spaces. I think your proposal > opens up a can of worms,in the end, once an exception is tolerated. 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. > I am not sure whether your idea really works this way. One should implement > a translator that produces adapted output on the web sites only, to > accomodate to common styles in particular fields of mathematics. 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. It's better to use names to hint to the reader the class purpose. We already do this throughout set.mm; "P" means the "set of points" for example in the Elementary Geometry section. But only having A through Z means that every class seems to be unrelated to each other; the lack of prime notation makes it impossible to hint to the reader about correspondences in a way that is typically done in math texts. --- David A. Wheeler -- 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/E1jujrL-00061e-No%40rmmprod06.runbox.
