The Coq mailing list

[Jake Ehrlich <jake.h.ehrlich AT gmail.com>]

HI guys,

I'm an undergraduate from K-State trying to understand the typing rules for Coq/Gallina and found these rules online: https://coq.inria.fr/refman/Reference-Manual006.html#sec170

The Prod rule seems to odd to me however. Consider type checking the term "nat -> Prop". This should clearly be of type "Type" and indeed coqtop tells me this is the case. However the 3rd Prod rule (The one dealing with Type) seems to suggest that "Prop" should have type "Type" and that "nat" should have type "Type" as well. Prop does have type "Type" but "nat" has type "Set"! That seems to mean that "nat -> Prop" should not be well defined! Of course "nat -> Prop" is well defined so either I am reading the rule wrong or the rule it self on that page is wrong but I am unsure as to which is the case. More than likely I am just reading it wrong but what exactly am I reading incorrectly here? How should I be reading this rule?

Thanks,

Jake Ehrlich