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
>
>
------------------------------------------------------------------------------
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
