The Coq mailing list

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

> You cannot. Eta allows you to identify very similar
> functions but not,
> say, quicksort and bubble sort.

What about the following argument taken from
Wikipedia?

if  f a==g a  for all lambda expressions a, then in
particular by taking a to be a variable x not
appearing free in f nor g we have  f x == g x  and
hence  ? x. f x == ? x. g x,  and so by eta-conversion
 f == g.



        

        
                
___________________________________________________________________________ 
Découvrez un nouveau moyen de poser toutes vos questions quelque soit le 
sujet ! 
Yahoo! Questions/Réponses pour partager vos connaissances, vos opinions et 
vos expériences. 
http://fr.answers.yahoo.com ;