Re: [mizar] Private DB

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

On Thu, 28 Sep 2006, Freek Wiedijk wrote:

> > I quite fear that e.g.
> >
> > extends JORDAN, OSAFREE;
> > notations SCMRING4;
> >
> > will be even more cryptic to the users than the current
> > "rococo", unless the overloading "behaves well".
>
> You have a point there.  Still, I think that even if it's not
> perfect, it will be at least much better.  So why not have
> this until something even more better comes along?

These are two competing philosophies, the one you did not mention says 
"make it right first time if you can".

I think what would be OK now, is having "extends" with just one article. 
I.e. yes to "extends JORDAN;" and no to "extends JORDAN, OSAFREE;". I am 
still not sure that even allowing the "notations" (and some other) 
directive after "extends" would be OK (maybe yes). The risk is again that 
you get a "nice short text" whose semantics is hard to decipher.

> > and automatically add it all to the "theorems" directive.
> >
> > And again, problem is that you may also need to add some "constructor"
> > directives for that
>
> So this third proposal was meant to be independent of the
> other two.

Yes, but if you want to "do it right", (i.e. as you said, the system 
should "figure out by itself what theorems you use") then it probably is 
not independent :-(.

> It _just_ was meant to not have to add stuff to
> the theorems line all the time.  So the way I imagine you
> would use a system in which the theorems line takes care of
> itself, is that you use it _exactly_ like you use the system
> today... only you don't have to write the theorems line.
>
> 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 say: just
> take one clear easy step, even when it doesn't get you
> _really_ where you want to be.  And then at least it be a
> little better.

I agree that just the simple automated care of the "theorems" (and 
"schemes") line adds more user comfort, and is easy to do. Sometimes the 
users will probably end up with something like a "constructors missing" 
error, but that should not be as frequent as the error you get now by 
omitting the theorem directive.

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

Josef