You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
When I wrote a lot of docs long time ago I typically used "∅" and "→" instead of "0" and "-->", and in the docs as well. Now I am wondering whether we should just uniformly use the simpler "0" and "-->" instead (except for the part where we show that the special version are possible.
I don't have any strong opinions, but and currently using "0" and "-->" in new stuff I write. @isaacsas If you prefer it that way I'm happy to change to these version next time I go through and make a doc change.
The text was updated successfully, but these errors were encountered:
When I wrote a lot of docs long time ago I typically used "∅" and "→" instead of "0" and "-->", and in the docs as well. Now I am wondering whether we should just uniformly use the simpler "0" and "-->" instead (except for the part where we show that the special version are possible.
I don't have any strong opinions, but and currently using "0" and "-->" in new stuff I write. @isaacsas If you prefer it that way I'm happy to change to these version next time I go through and make a doc change.
The text was updated successfully, but these errors were encountered: