The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

roconnor AT theorem.ca
 wrote:

> It seem that Coq ought to define -> to have kind type -> type -> type, 
> and/or implement eta-equivalence.
So you want to define the type of -> in terms of itself?  That sounds 
messy, and even more so since it is just syntactic sugar for 'forall'.