Hi Thomas,
Thanks for your reply.
I mean that I have a set: pop, the datatype of the element of pop is ch.
Firstly,the pop is unordered,the number of ch IN pop.j is different. Secondly,
I use length to compute a real list and get a real(e.g.val value_def =
Define`value ^ch ^pop = !num1 num2. ch IN pop.length [num1;num2] = num1 +
num2`;). Thirdly,according to the length, I need a sorting operation.
Finally,the big the length, the small the number of ch.j.
Maybe, I also need some implementation of finite sets that use an order of the
elements to refer, could you give me some examples?
Best
Liu
------------------------------------------------------------------------------
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
