A proposed syntax for binders in Mizar
Freek Wiedijk · 2003
Abstract. Binders like ‘lim ’ (for limits), ‘ � ’ (for summation) and ‘ � ’ (for integration) are an essential part of the language of mathematics. They are the ‘higher order ’ elements of mathematical expressions. At the TYPES meeting of 2003 in Turin, Andrzej Trybulec told me that the reason that Mizar did not have binders was that nobody had proposed a good syntax for them yet. To take this reason away, we will present a syntax for binders in Mizar.