The Coq mailing list

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

Does it mean that I cannot generalize my lifting
function to dependent types?

--- 
roconnor AT theorem.ca
 a écrit :
> 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.




        

        
                
___________________________________________________________________________ 
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