Re: [mizar] Was it meant to be that way?

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

On Mon, Jan 26, 2004 at 03:46:48PM +0100, Andrzej Trybulec wrote:

> Yes. The free variables in the definiens are bound by default. The order of
> binding depends on the order of the
> reservation. So the definitional theorem is
> 
>      for X,p holds X |= p iff for A,v,J holds J,v |= X implies J,v |= p
> 
> and in
> 
>       for X,p holds X |= p iff for A,v,J holds J,v |= X implies J,v |= p
>       for A, J, v holds J,v |= X implies J,v |= p
>   ---------------------------------------------
>                          X |= p
> 
> pattern matching fails. It is one of many things that I would like to change in
> Mizar, but with a very very low
> priority: you do not know how the default mechanism works, do not use it.

Nice piece of advice.  But it was someone else that wrote the
definition and I only tried to use it.  I could have even heard about
the default yet I needed an hour to sort it out.  This is a small trap.

I have noticed that many authors state all quantifiers explicitely.

Cheers,


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