Re: [mizar] Strong Mizar wish: linking to consider (fwd)

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

Freek Wiedijk wrote:

>
> I even guess that it might sometimes not even be possible to
> print a term in such a way that parsing it will give you the
> original term back (when some newer constructor shares the
> notation with the one that you are trying to print.)
>

You mean in a new environment, this is right. We need a new concept "the
correctness of the library", to eliminate the "an illegal overloading".
But this is a task (to eliminate it) for the Library Committee, not for
an individual user.


>
> The Mizar checker mizf doesn't need to care about this,
> because all it ever prints is error numbers.  But if you want
> a system that prints more information than that (most systems
> do, and I expect HELM = MoWGLI wants be one of them), then
> this might be a problem.  If you don't mind the "output" not
> to be usable as "input" again, there's no reason to worry.
> But _I_ like to be able to occasionally cut-paste stuff back
> into my source files.

Could you give an example.

Greetings,
Andrzej