Re: [mizar] be and being

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

Hello,

On Tue, 16 Dec 2003, Piotr Rudnicki wrote:

> Therefore I propose that both 'be' and 'being' have an alias ':'
> which is shorter and commonly used in this context in everyday
> writing, not to mention some other system that use it.

I'm afraid this would interfere a bit with labels. Mizar grammar allows
for labels with ':' separated from the 'stem' by spaces.
Although the context should tell clearly what is actually meant, errors
recovery would probably suffer on that change.

> I have been typing quite a lot in Mizar recently and the sheer length
> of the tokens 'being' and 'be' sort of bothers me.  In addition, MML
> has
>
> 	at least 10554 occurrences of "for ... be ..."
> 	at least  5146 occurrences of "consider ... be ..."
> 	at least   141 occurrences of "given ... be ..."
> 	at least   869 occurrences of "let ... being ..."
>
> It is not particularly important but looks ugly.

Some time ago Artur Kornilowicz wrote a utility which corrects those
'ugly' uses of be/being, but it seems that the Library Committee does not
use it consequently during submission of new articles.

Adam Naumowicz

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================