Re: mode definition/"the" question

On Fri, 26 Aug 2011, Artur Kornilowicz wrote:

> Hence, having
>
> Lm2: the FOO1 is empty by DefFOO2;
>
> Mizar does not know how IT could be substituted - there is no term of type 
> FOO2 around.
>
> The solution is to add a reference to a statement with a variable of type 
> FOO2, for example:
>
> the FOO2 = the FOO2; then
> Lm2: the FOO1 is empty by DefFOO2;

This example shows that it might be useful to automatically add all the 
global choice terms for the types occurring into the universe of 
discourse. But the question is how useful it would be in general and what 
would be the cost of the extra processing in the checker.

Best,

Adam

=======================================================================
Dept. of Programming and Formal Methods  Fax: +48(85)7457662
Institute of Informatics                 Tel: +48(85)7457559 (office)
University of Bialystok                  E-mail: [email protected]
Sosnowa 64, 15-887 Bialystok, Poland     http://math.uwb.edu.pl/~adamn/
=======================================================================