Re: [mizar] Binders?

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

On Mon, Oct 14, 2002 at 04:35:45PM +0200, Freek Wiedijk wrote:

> I'd like to write a sum in the style "sum(i=1,n,i^2)", so
> where the i "binds" (instead of "sum f" where somewhere else
> it is said that "for i holds f.i = i^2", which is much more
> clumsy.)  The same thing is needed for things like limits,
> integrals, etc.

Interesting, I always thought that "sum(i=1,n,i^2)" was clumsy in comparison
to "sum f".

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