The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I feel that people who are unfamiliar with the propositions-as-types philosophy

might consider the notation 

(n : nat) -> (Vec n)

more natural  than 

forall (n : nat), (Vec n)

Is there some way in Coq to write dependent

function types in the former way?

Regards,

-- Abhishek

http://www.cs.cornell.edu/~aa755/