Re: [mizar] puzzle

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

On Sat, Nov 02, 2002 at 12:50:17PM +0100, Freek Wiedijk wrote:
> Adam:
> 
> >As these are rather technical notions, maybe it would be
> >better to replace them by less ambiguous symbols ?
> 
> I agree.  I always have the same feeling with ^2 for square.
> The functor should be ^ with 2 as the argument.

These are good examples of violating what Andrzej christened "integrity"
(for the lack of better term) of MML at the lexical level.  This definitely
should be revised.

My mishap was with [x] from CAT_4.  Use P[x] and you will see.
c= is also a candidate, I think, but there are some arguments in
favour of keeping it.  It is fortunate that we do not have U for union
anymore.

Cheers,


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