Re: [mizar] Hindrances

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

Piotr Rudnicki wrote:

>
> Some time ago, Andrzej suggested "hindrances" with understanding
> "hindrances to MML maintenance".  We finally used "integrity" in a
> paper for MKM.  Frankly, I do not like either of these names.
> "Smoothing rough edges" describes what is the essence of the issue but
> is still no good as a name for the problem.

Piotrze,

I have never suggested that. I talked about hindrances to using MML while writing
an article. Hindrances make the proofs longer, sometimes unable to write a proof
in a reasonable manner. It happened.

And integrity is something else. I do not say that it has nothing to do with
hindrances, but definitely
it is NOT that
            "the integrity" = "the lack of hindrances"
at least in the meaning that I try to assign them.

Greteings,
Andrzej