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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and