Re: [isabelle] finite sets and code generation, once again

Hi Peter,

> What's about
>     d) Parameterize over choice-function (e.g. using a locale, fixing
> choice and assuming: "s~={} ==> choice s : s"), do your definition
> inside this locale
>         and then instantiate to concrete set implementation ?

yes, that is also a possibility.  (I had the already the strong
impression that I missed something).

Thanks for pointing this out.




PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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