Re: [isabelle] Sets



Dear Hidetsune,

>   Let A be a set (A :: 'a set), then is there a 
> set (B :: 'b set) which is isomorphic to A?

Not in general.  The type 'b might be too small to accommodate all the
elements of A.  This doesn't hold because type variables are implicitly
universally quantified at the very beginning of a formula.

Clemens





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