The Coq mailing list

[Murali Vijayaraghavan <vmurali AT csail.mit.edu>]

Hi

I was wondering why the following definition fails:

Inductive Foo: Type :=
| Simple: nat -> Foo
| Bad n (vals: (fix helper n :=
                  match n with
                  | 0 => unit
                  | S m => (Foo * helper m)%type
                  end) n): Foo.
Error: Non strictly positive occurrence of "Foo" in

"forall n : nat, (fix helper (n0 : nat) : Set :=

                    match n0 with

                    | 0 => unit
                    | S m => (Foo * helper m)%type
                    end) n -> Foo".

From my understanding, strictly positive occurrence requirement is violated if I supply the inductive type as an argument to one of the constructor arguments (as discussed in http://adam.chlipala.net/cpdt/html/Cpdt.InductiveTypes.html#lab30), but in the above example, I am just trying to use an size-indexed tuple as a constructor argument. How can I prove False if the above definition were accepted?

Thanks

Murali