mn200/HOL — Issue #51: Binder-like syntax for {PROD,SUM}_IMAGE
Author: mn200
Created: 2012-01-11 03:12:25+00:00
State: open
Labels: Feature Request, Printing-Parsing

`Π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 `::`).