Re: [isabelle] Finite set datatype?

Hi Palle,

> So yes, is there an actual finite set datatype, or would it be possible
> to define one?
> Or must I use lists in the nominal datatype to somehow emulate finite sets?

> There is the theory Fset in library which defines a finite set type.

I actually must correct my quite misleading heading of this file: the
type fset itself is indeed infinite.

Christian hints should indeed suffice.

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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