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

[Freek Wiedijk <freek@cs.kun.nl>]

Josef:

>Without information about this level, it is impossible to do
>some transformations of the presentation correctly.

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.)

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.

By the way, Coq also has the problem that it sometimes isn't
able to parse the terms that it has printed itself (because
it gets confused about the coercions, I think).  Randy
Pollack thinks it's a serious shortcoming of Coq.  "How are
you to know what Coq is doing inside, and therefore trust
that you have proved what you think you have proved, if what
Coq prints can be wrong?"  Or something like that.

Freek