Re: Extended ASCII

[Andrzej Trybulec <trybulec@wwwserve.cs.shinshu-u.ac.jp>]

Piotr Rudnicki wrote:
> Adam Grabowski wrote:
> 
>  > I haven't any good idea what to put in place of #237
>  > (emptyset seems too long, maybe 0?) or #238 (membership
>  > relation - in?). Such a change could be annoying to experienced
>  > Mizar users so it should be discussed.

I would not start with #237 (empty set), #238 (membership) or
 #239 (meet), or even #249 (central dot, usually multiplication).
There is a lot of funny notation in Mizar, that has nothing common with
regular mathematical notation (PRALG_1:def 3,def 21, PRALG_2:def 10,
def 11  or TREES_1:def 12, TREES_2:def 12, TREES_A:def 1,def 2,def 3)
that should be changed ASAP.

> Probably 0 will win but I would like \0 better.

Freek Wiedijk wrote (don't look for it in the Mizar Forum archive,
a private message)

"Wouldn't that change the type of "0" or of empty set?  Or do
they currently have the same type already?  (I would expect,
currently, that it would be "Nat" vs. "set", but maybe that's
not true?)"

And I believe that it may be a real problem, I could not anticipate
semantic problems that may arise when we identify the symbol for the
empty set and zero. What if MML crashes?

However, also there is, maybe not so serious, problem with editing. It
would be good to enable authors to use either such symbol that will be
published as zero or such that will be printed as empty set. Even if
they are synonyms.

So maybe \0 as Piotr proposes, or [] - used now for the empty function,
or just {} - easy to remember?

> Are there any suggestions for extended-ASCII symbols from HIDDEN?

Basically we discussed all symbols on HIDDEN.VOC. There is U umlaut
#154, it is not used at all. We put it put on HIDDEN.VOC, because we
wanted to substitute it for "U" (the symbol for binary union).
Fortunately we never did it.

Well, I forgot, #242 and #243, for them we can substitute "<=" and
">=". Is something else on HIDDEN.VOC?

Andrzej Trybulec