The Coq mailing list

[roconnor AT theorem.ca]

I was trying use the type constructor (expr->), wanting it to have kind 
type -> type, but this of course does not work.

Instead I am forced to write the eta-expanded version (fun A => expr->A). 
This strikes me as potentially akward.  It seem that Coq ought to define 
-> to have kind type -> type -> type, and/or implement eta-equivalence.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''