Thanks. On 21/02/18 11:57, Thomas Tuerk wrote: > Hi, > > the simplifier supports AC normalisation (see Sec. 7.5.5.2 in the > description manual). AC normalisation would sort multiple occurrences of > the same operant next to each other. Therefore these multiple > occurrences can then be removed by providing 2 idempotency rewrite rules: > > f x x = x > > f x (f x y) = f x y > > This provides a very high level simple way to do what you want, I believe. > > If you want something lower level, more efficient with finer control, > you could use "sort" from structure "AC_Sort". It provides a conversion > that does what you want if instantiated properly. However, I never used > it myself, so I don't have first hand experience with it. > > There is also the structure "AC" from refute. However, I believe in > contrast to "AC_Sort", there is no direct support for idempotency in "AC". > > Cheers > > Thomas
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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
