The Coq mailing list

[Benjamin Werner <benjamin.werner AT polytechnique.fr>]

  Hi,

I am not the most qualified person to answer. I do not think
there is some "anti-eta" clique at work in the Coq development.
 It is rather that the practical problems caused by the absence
of eta-conversion (and thus the pressure to introduce it)
were not yet strong enough for anybody making the effort
to do it.

So this discussion seems to yield a "practical" reason to add it :-)


Cheers,


Benjamin


> > So an interesting question is: why is eta-conversion still not
> > considered in Coq's conversion test?  Hmm... I think that this
> > situation is due to historical reasons.  Only.    :-)
>
> I tend to agree with him. So let me repeat his question:
> why is eta-conversion still not considered in Coq's conversion test?
>
> Bas
>
> -------------------------------------------------------
> Research Group Foundations/ Institute for Computing and Information 
> Sciences
> Radboud University Nijmegen www.cs.ru.nl/~spitters/
> P.O.box 9010, NL-6500 GL Nijmegen, The Netherlands.
> spitters AT cs.ru.nl
>  Ph:+31-24-3652631 F:+31-24-3652525 Room: A5024
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club