Among others, LENGTH (FILTER (\e. X = e)) = 1 Scott
> On 2017/10/05, at 15:55, Chun Tian (binghe) <[email protected]> wrote: > > But my list is not ALL_DISTINCT … there’re duplicated elements for sure, just > the appearance of certain element is only one. —Chun > >> Il giorno 05 ott 2017, alle ore 16:48, Konrad Slind <[email protected]> >> ha scritto: >> >> Hi Chun Tian, >> >> The constant ALL_DISTINCT in listTheory is what you are looking for, I >> think. >> >> Konrad. >> >> >> On Thu, Oct 5, 2017 at 9:03 AM, Chun Tian (binghe) <[email protected]> >> wrote: >> 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 >> [email protected] >> https://lists.sourceforge.net/lists/listinfo/hol-info >> >> > > ------------------------------------------------------------------------------ > 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 > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
