mn200/HOL — Issue #52: Consider making MEM e list an abbrevation for e ∈ set list
Author: mn200
Created: 2012-02-01 05:03:23+00:00
State: open
Labels: Feature Request, Printing-Parsing

The use of `∈` rather than just application (*i.e.*, `set list e`) is necessary to get things like `MEM e (list1 ++ list2)` to expand nicely.

It seems clear that the abbreviation has to be this way round. The alternative the other way would be to have `set list` map to `{ x | MEM x list}`, which is surely too complicated.

I will look into how much this change would break.