Hi, I need to express the fact that the elements in a list are all identical, what’s the suggest way? Currently I have this: (inspired by ALL_DISTINCT)
val ALL_IDENTICAL_def = Define ` (ALL_IDENTICAL [] = T) /\ (ALL_IDENTICAL (h :: t) = if NULL t then T else (MEM h t /\ ALL_IDENTICAL t))`; But the definition is ugly and a little long. Any suggestion on a better definition? Thanks. Regards, Chun Tian
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
