Re: [mizar] Scheme for func definition with Fraenkel operator?

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

On Mon, Jan 06, 2003 at 01:54:59PM +0100, Freek Wiedijk wrote:

> Something related that _would_ be nice is to have "by"
> strengthened in a way that:
> 
>   a in { x : P[x] } 
> 
> implies
> 
>   P[a]
> 

This can be syntactically incorrect in case 'a' is of an inappropriate type. 

> instead of only
> 
>   ex x st a = x & P[x]

while this is always fine.

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