The Coq mailing list

[Christine Paulin <paulin AT lri.fr>]

I think this development comes from an earlier version of Coq in 
which the cumulativity rule 
        A:Set 
       ------
        A:Type
was not implemented, the proof should go now without having to use an 
extra Nat type.

Christine Paulin.

In his message of Mon June 8, 1998, Paul van Wamelen writes: 
> Hello all!
> 
> Why is "nat" defined to be of type "Set"? 
> 
> In the file 
>   V6.2/lib/coq/theories/SETS/Integers.v 
> there is a proof of the fact that the natural numbers (why is the file
> called "Integers.v"?) is an infinite set. But a lot of energy is
> expended to first set up a bijection between "nat" and "Nat" of type
> "Type", so that we can now work with the "Ensemble" of natural
> numbers. It seems that if we originally defined
>   Inductive Nat : Type := NatO : Nat | NatS : Nat -> Nat.
> this proof at least would have been much easier. Are there other
> things that you would then not have been able to do?
> 
> Sincerely,
> Paul van Wamelen.

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, URA 410 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86
  INRIA tel : (+33) (0)1 39 63 55 70       fax : (+33) (0)1 39 63 56 84
  Tatoo tel : 06 04 24 44 75 
   message numerique +1(pas urgent)-3(tres urgent) ou * + message vocal