[isabelle] finite sets and code generation


I am curious to know what the code generator can do with finite sets.

For proof re-use reasons I use this idiom to fudge them into lists (in a definition context):

xs_list = (SOME xs. set xs = { my finite set })

The only substantial reason I have is that I can make use of the equivalence relation partition operator '_ // _' on these sets.

Is there a way (does someone have some code) to partition lists? Is there a more-complete treatment of finite sets for the code generator somewhere?



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.