Re: [isabelle] finite sets and code generation


On 04/03/2010, at 8:21 PM, Daniel Wasserrab wrote:

> perhaps you might want to take a look at a publication from my colleague:
> Andreas Lochbihler: Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL. TPHOLs 2009
> He describes how to generate code for finite functions in Isabelle and also gives an example for finite sets. This work is also accessible in the AFP:

Thanks for this! I am embarrassed that I didn't consult the AFP before sending that email

(Co)Incidentally this will at least solve another problem I was facing, viz dealing with functions over finite subsets of some arbitrary type, which may or may not coincide on the rest of the type... a problem I didn't expect to be so neatly treated as it is here.

Rene: thanks for your kind offer. I will see how Andreas's FinFuns work out.



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