Re: [mizar] unused loci

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

On Thu, 22 Feb 2007, Adam Naumowicz wrote:

> The implicit parameters must be somehow deducible from the explicit ones - 
> that's the case with 'p' which is reconstructed using 'c'. Otherwise there's 
> no way to specify which 'f' you have in mind when you use 'Sum c'.
> And if you mean 'any f', then it must be stated as such in the definiens:
>
> func Sum c -> Element of F2 means
> for f being enumeration of vertices(p) ...
>
> or as you propose (which is even better to use later)
>
> func Sum c -> Element of F2 means
> for f being enumeration of vertices(p) ...

Of course I meant here:

func Sum c -> Element of F2 means
ex f being enumeration of vertices(p) ...

Best,

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/
======================================================================