The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 01/09/2015 22:22, Jake Ehrlich wrote:
> More than likely I am just reading it wrong but what exactly am I
> reading incorrectly here? How should I be reading this rule?

You're actually reading it right. What you lack to type nat -> Prop :
Type is the cumulativity rule (which is indeed described in the page you
linked). It allows to upcast types into higher universes ; in your case,

nat : Set <= Type

so

nat : Type

and your arrow is typeable as expected.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature