Hi,
(I'm new to HOL's listTheory). Suppose I have a list L which contains
possibly duplicated elements, and I want to express certain element X is
unique (i.e. has only one copy) in that list. How can I do this? It seems
"?!" doesn't work here, e.g. ``?!e. MEM e L /\ (e = X)``.
Regards,
Chun Tian
--
Chun Tian (binghe)
University of Bologna (Italy)
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
