The Coq mailing list

[Fabrice Lemercier <nouvid-coq AT yahoo.fr>]

Hello,

One can lift a function of type  A->B  to the type 
(option A)->(option B) by:

  Definition lift (A B:Set)(f:A->B)(a:option A) :
option B :=
    match a with
      Some a' => Some (f a')
    | None => None
    end.

I would like to generalize it to dependent types. 
First I need to figure out what would be its type.  I
assume parameters

  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).

But Coq replies:

  User error: Inference of annotation not yet
implemented in this case

So, what's the type?

Thanks,

Fabrice.



        

        
                
___________________________________________________________________________ 
Nouveau : téléphonez moins cher avec Yahoo! Messenger ! Découvez les tarifs 
exceptionnels pour appeler la France et l'international.
Téléchargez sur http://fr.messenger.yahoo.com