[mizar] Binders?

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

Hello,

A short question: have there ever been experiments in Mizar
with "binders"?

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.

So in higher order systems it is more or less automatic that
you have this (apart from notation), but I expect that in
Mizar it also should be possible to make sense of something
like this.

So has someone ever looked into whether it would be possible
to add something like this to Mizar?

Freek