coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: Unification problem in Coq?

From: Bas Spitters <B.Spitters AT cs.ru.nl>
To: Benjamin Werner <benjamin.werner AT polytechnique.fr>
Cc: herman geuvers <H.Geuvers AT cs.ru.nl>, Coq <coq-club AT pauillac.inria.fr>, formmath AT cs.kun.nl
Subject: Re: [Coq-Club] Re: Unification problem in Coq?
Date: Tue, 26 Apr 2005 22:56:03 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Monday 25 April 2005 15:12, Benjamin Werner wrote:
> 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 :-)

Thanks for your answer.

It would certainly be convenient to have eta-conversion.

Bas

[Coq-Club] Unification problem in Coq?, herman geuvers
- [Coq-Club] Re: Unification problem in Coq?, Bas Spitters
  - Re: [Coq-Club] Re: Unification problem in Coq?, Benjamin Werner
    - Re: [Coq-Club] Re: Unification problem in Coq?, Bas Spitters