Opened 4 years ago

#13 new enhancement

Set comprehensions with patterns

Reported by: tilk Owned by:
Priority: major Component: Proof Engine
Version: Keywords:


Currently, one can only write set comprehensions like this: {x \in S | F}, where x is a variable. I should be able to write any pattern there, like for example {<a,b> \in S | F}. It probably should be a syntax sugar for {x \in S | \exists a \exists b (x=<a,b> /\ F)}.

Additional requirement: if a variable occuring free in the pattern is bound in the assumptions, it should NOT be bound in the pattern.

(Ticket moved from

Attachments (0)

Change History (0)

Add Comment

Modify Ticket

as new The ticket will remain with no owner.

E-mail address and user name can be saved in the Preferences.

Note: See TracTickets for help on using tickets.