Binder-like syntax for {PROD,SUM}_IMAGE

[mn200]

Πx ∈ s. x + 1 should parse to PROD_IMAGE (λx. x + 1) s. This is very similar to the transformation done in handling restricted quantifiers (which should also have their syntax extended to allow for ∈ as well as ::).

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[mn200]

It's possible to almost get there already with the following:

new_constant("sigma", ``:'a -> num``);
set_fixity "sigma" Binder;
associate_restriction ("sigma", "rsigma");
overload_on ("rsigma", ``\s f. SUM_IMAGE f s``)

You can then write sigma n::s. n * 2 and get back the term SUM_IMAGE (\n. n * 2) s. Unfortunately, the pretty-printer dies, but the parser does the right thing.

The sigma constant is entirely fake and unnecessary. It's possible that the new_constant line could be entirely omitted.