The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

ne Vestergaard wrote:

> When inputting "Print nat_rect." to the current Windows version (8.0, 
> April 2004), I get the following response:
>
> nat_rect =
> fun (P : nat -> Type) (f : P 0) (f0 : forall n : nat, P n -> P (S n)) =>
> (fix F (n : nat) : P n :=
>    match n return P with
>    | O => f
>    | S n0 => f0 n0 (F n0)
>    end)
>      : forall P : nat -> Type,
>        P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
>
> Should it not be "match n return (P n)"?


Yes, in coq8.0pl2,

it's  "match n as n0 return (P n0)  ... "

and when I check he term you mention on  V8.0pl2, I get the message :
The term "P" has type "nat -> Type" while it is expected to have type
"Type"

Pierre




> Cheers,
> /R
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club