Re: [mizar] Binders?

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Piotr,

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

So I feel the other way around.  The first notation becomes
even nicer when you nest binders.  To write a lemma
"sum(i=1,n,sum(j=1,m,a[i,j])) = sum(j=1,m,sum(i=1,n,a[i,j]))"
the second way will be a _lot_ less transparent, I think.
Just tell me how you would write this scheme in the "sum f"
style, and we'll see.

(Of course if you have lambda abstraction, _then_ the first
is just an instance of the second.  But Mizar hasn't, not in
a way that makes this "binder" notation look nice (or has it?))

Another argument for wanting binders is that it conforms to
"normal" mathematical practice.  Mathematicians never write
lambdas for functions (so they don't have lambda-binders),
but they certainly write sum-signs that bind variables.

Freek