Re: [isabelle] the hereditarily finite sets



Thanks, but I believe that you are describing finite sets rather than hereditarily finite sets. I should have mentioned, the membership function should have the following type:

	member  :: hf => hf => bool

That is, we have one single type rather than separate types of sets and elements.

It sounds like this hasn't been formalised before...?

Larry

On 25 Mar 2012, at 20:18, Andreas Lochbihler wrote:

> Hi Larry,
> 
> The FinFun formalisation in the AFP contains until Isabelle2011-1 defines such a type in theory FinFunSet. Adapting it to the pred/set-distinction, I recently (ID b7aa87989f3a) changed it from sets to predicates, so it is called FinFunPred in the development branch of the AFP.





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