Re: [mizar] Private DB

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

Hi Josef,

>>You seem to want to take many improvement steps together,
>
>Might be restated as that I am trying to find what the real
>problem is :-)
>
>>and then you complain that it will become a mess.
>
>and actually also try to find a solution to it :-).

I think that I myself only will like the solution if it's
"backward compatible".  If I won't be able to write my terms
the way I can now because the mechanism will be more
restrictive, for me it won't be a good solution.  In that
case the solution will be worse than the problem.

>Sometimes the users will probably end up with something like
>a "constructors missing" error,

But now they will get exactly that same error too, at exactly
the same moment in writing the formalization.  So that is not
a difference with the current situation.

>I am not sure that there is a good separation between the
>header problems and the overloading problems.

Of course there is separation!  Of my three requests, only
the second one seems to have some interaction with your
overloading doubts (because it's not clear how the different
notations imports flow together).  The "everything" proposal
and the "theorems" proposal are not _at all_ unclear because
of the strangeness of how overloading currently works.

I still thing the environ mechanism can be a lot easier
already without having to find out in what way it really is
"right".

Freek