Re: [isabelle] Silly problem with maps and



On Wed, 2009-07-15 at 10:46 -0400, John Ridgway wrote:
> In the original you don't even need to play with sizes;
> all you need to do is assume that SOME l is l.

Well, to obtain a counterexample to an implication, one must not just
falsify the conclusion, but also satisfy the premises.  In the original
this requires 'a to have (at least) 2 elements.  In contrast, the range
type 'b of M may be a singleton.  That's just what the message "Size of
types: 'b: 1 'a: 2" indicates.

Regards,
Tjark






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