[mizar] Medice, cura te ipsum

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Piotr Rudnicki wrote:

> It seems  that there is some discussion that is done in private while
> it should be a public one. e.g. a lot of e-mail exchanges between
> Freek and AT about Mizar from a year ago or so.  The entire community
> would have benefitted a lot if they talked over the mizar-forum forum.
>

I completely agrre. Some years ago I had refused to read cc's of a discussion
between Piotr Rudncki and John Harrison because I believed  (I stiil believe) it
should take place on qed.

Recently, Zhaohui Luo commented important posting of de Bruijn, and, of course,
Luo send me it by private message.

Piotr Rudnicki and Adam Naumowicz recently discuss semantics and syntax of
Functor Cluster Registration,
inprivate.



>
> Recently, Robert Solovay and AT had some e-mail exchanges that I think
> properly belong to the mizar-forum as their correspodence is of
> general interrest.

Not true, it has been published on Mizar Forum.


Andrzej Trybulec