Re: [mizar] Proposal for binders in Mizar

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

Hi Josef,

>I was also a bit puzzled by the intended meaning of the
>"lambda" variables in the binder definition, but now it
>seems to me that they are there just to define the
>syntactical pattern of the binder, and cannot be used in its
>definiens. You can only use the "at" variables there,
>right?

Yes.  So these variables are not bound by a "let" either, and
I feel you shouldn't need a reservation for them if you don't
give the type, as it will be clear from the f(...) parameter.

>(actually "equals" definition could also be possible)

I had an example of that in my second "sum" definition.

>I was just interested in the semantics, I have no problem
>with "\" instead of "lambda", or even more syntactic sugar
>like the "at" construct.

But then I wonder how you'd write the definition.  For
instance, can you give an approximation of what the
definition of the "... at ... of ..." syntax for a "sum"
binder would look like if it were defined in your style (so
as a function "sum" applied to a lambda)?

>I just do not like the current lack of typing for the
>Fraenkel terms,

I agree with that.  Although it's not clear to me what the
"better" typing rules should be.  (If the type of the
parameter is Element of A, I probably would like the Fraenkel
term to have type Subset of A.  But apart from that I don't
know how it should work.)

Freek