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 <konrad.sl...@gmail.com> > 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) <binghe.l...@gmail.com> > 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 > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > >
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ 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
