+g: Primarily ".+". For 'second' additions (like in homomorphisms), use ".+^".
> and .0 instead of .0. (I know David
> objected to the latter...
I still object to this one :-). Yes, obviously the *computer* can tell the
difference, but I think it's important that *new* authors can obviously tell the difference.
If you haven't already, I strongly recommend that you document this
somewhere other than this email. Perhaps viewable metamath comments
in set.mm. That way future readers can see the current conventions.
On 3/6/16 7:57 AM, Mario Carneiro wrote:
Here are the conventions I
used:
+g: Primarily ".+". For 'second' additions (like in homomorphisms), use
".+^". For derived structures (like quotients or power structures) use
".+b". (Using ".+" is preferred over multiplicative notation even for
noncommutative groups.)
.r, .s, .g: Primary ".x.", secondary ".X.", derived ".xb"
*r: Primary ".*", derived ".xb"
LSSum, GrpAct: Primary ".(+)", derived ".+b"
I don't recall ever seeing .(+) used for LSSum; it always seems to be a plain overloaded + sign. I have seen (+) used only for direct sum - see e.g. 'direct sum of modules' on Wikipedia. My intent was to reserve .(+) for direct sum and use .+b for subspace sum.
If you can find a reference that uses (+) for subspace sum, I'll withdraw this objection.
I added .0b to set.mm for future use.
I prefer ._|_ and think that "quite long" is mostly an optical illusion due to the long underscores. In monospaced font it takes exactly the space of .(+) and is instantly recognizable. It also conforms to our informal rule, "existing symbol prefixed with .".
(BTW our use of a full-sized _|_ as a prefix function rather than a superscript is not without precedent. See for example Mittelstaedt's _Quantum Logic_ p. 9.)
+g: Primarily ".+". For 'second' additions (like in homomorphisms), use ".+^".
For homomorphism I definitely suggest indices, It is easy to create using the gifs, and you can add as many of them as you want. It is also true for the zeroes. The apparence in the metamath site is good: the figure isput in lower position.
The converted set.mm is on us2 now.
I'm still not thrilled with the dotted underline as the disambiguating decoration. For example look at http://us2.metamath.org:88/mpeuni/hlhilphllem.html - at first glance the underlined + sign almost looks like a +/- sign. Overall it just seems a little distracting for pleasant readability.
We have done many experiments and dotted underline was the one that I (and I think Mario) disliked the least, but we can always change our minds if someone has a better suggestion. It is just a matter of editing the css in the set.mm $t comment if anyone wants to experiment.
I set up mmsetalt.css to turn off the underline on Unicode pages for comparison. Select View -> [Page] Style -> mmsetalt in Firefox and IE.
The hlhilphllem page also has center dot ".x." and comma ".,". In FF Unicode these are small and faint and hard to distinguish, whereas in IE they are rendered more solidly and are easily visible. It seems a font doesn't completely define how it's displayed, but I don't understand why.
By the way, Mario, my original intent was to use .+^ as vector sum and .+ as scalar sum, not the reverse. The .+^ has a little hat over it that's intended to suggest "vector" and is sometimes used on unit vectors i, j, k in elementary books. An arrow over the plus would have been my first choice but I didn't find it in the Unicode charts.
A symbol that is missing is a circle. It can be used for concatenation, categorytheory morphisms compositions and maybe similar operations.
For special cases like the "}{" here where the middle of the braces are too close, there is a hack in metamath.exe (mmwtex.c line 4901) that recognizes special combinations like this and adds a space independently of the htmldef for better appearance, that I fine tune over time. I'll add this case in the next metamath.exe.
The hlhilphllem page also has center dot ".x." and comma ".,". In FF Unicode these are small and faint and hard to distinguish, whereas in IE they are rendered more solidly and are easily visible. It seems a font doesn't completely define how it's displayed, but I don't understand why.They don't seem too significantly different on my machine (screenshots attached)...
On Mon, Mar 7, 2016 at 7:34 PM, Norman Megill <n...@alum.mit.edu> wrote:For special cases like the "}{" here where the middle of the braces are too close, there is a hack in metamath.exe (mmwtex.c line 4901) that recognizes special combinations like this and adds a space independently of the htmldef for better appearance, that I fine tune over time. I'll add this case in the next metamath.exe.Interesting, I didn't know you could do this. How about a $t command like:
kerning "}{" as " ";to allow for specifying these in the typesetting? (Other possibilities for the right side include thin spaces or multiple spaces, specified with HTML entities.)
Because I'm lazy and a crude hack is easier. :) Also, there are also more complex situations in there involving quantification where space or no space depends on the kind of symbol, e.g. space between the two x's in A. x x = y, meaning a command to specify that would require conditionals or pattern matching to symbol categories. It's just much simpler for me to hard-code the handful of cases directly in the code.
All this is fine in principle but would require a massive rewrite of the
code.
You have the patience of a saint. I hope you find this stuff rewarding at least part of the time.
--
Dan Connolly
http://www.madmode.com
You have the patience of a saint. I hope you find this stuff rewarding at least part of the time.
There is no dependency during web page generation. What you want should
be straightforward to achieve on your own.
No one is ever going to bother you in the middle of the night because a proof crashed. :)
I still think that simple facts like ¬ 2 ∥ 3 are useful as separate theorems, since:
1. it's unlikely most readers will *want* to see that particular proof ("it's obvious"), and
2. it's easier to reuse them that way.