The Coq mailing list

[roconnor AT theorem.ca]

On Mon, 23 Jan 2006, Fabrice Lemercier wrote:

>   Parameters (A:Set)(B:A->Set)(f:forall a, B
> a)(a:option A).
>
> And then I try
>
>   Check (match a with None => None | Some a' => Some
> (f a') end).

This doesn't work because the type of Some (f a') is option (B a'), so the
type of the entire match expression ought to be option (B a'), but this is
impossible because the a' would escape its scope of the second case of
the match clause.

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''