Re: [mizar] A quote

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

On Wed, Nov 19, 2003 at 01:04:16AM +0100, Josef Urban wrote:
> 
> On Tue, 18 Nov 2003, Piotr Rudnicki wrote:
> 
> > However, it is inevitable that people will be discouraged by the
> > amount of garbage in MML.  In this light the "weak types" can wait.
> 
> I have produced quite some garbage myself, in the osalg articles, because 
> of nonclusterable attributes. Fixing it now is fair amount of work.
> If someone wants to write garbage, you will not prevent him, but we should 
> work on improving the system, so that it does not _force_ you to write 
> garbage.

I would not call this garbage - just the sawdust when cutting trees,
inevitable, and as you write there will be less sawdust.  Such an
evolution of a system is inevitable, look at the changes in Coq 8.

What I had in mind is keeping in MML stuff that creates opinions like the
one that I cited in the previous message.

-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr