The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

I'm stuck again :-) Coq gives this error:

The term "Vector.cons nat (h + h') l' (fn h' l' t')" has type
 "Vector.t nat (S l')" while it is expected to have type "Vector.t nat len".

in this code:

  Definition pt_aux : forall (h len : nat), Vector.t nat len ->
Vector.t nat len :=
    fix fn h len v :=
      match v return Vector.t nat len with
      | Vector.nil => v
      | Vector.cons h' l' t'  =>
          Vector.cons nat (h + h') l' (fn h' l' t')
      end.

so I need to somehow tell Coq that S l' = len, because t' is tail part
of vector v and v has length len.

I tried implementing something like

  Definition vector_cases {T : Type} (len len' : nat) (v : Vector.t T len) :
    {ve : T * Vector.t T len' | len = S len'} + {len = 0}.

but this is obviously wrong, because I need to get len' as return, I
don't know if such a len' exists or if it does, whar is it. I don't
know how to encode this idea in Coq.

Maybe I should read one or two more chapters in CPDT :-)

---
Ömer Sinan Ağacan
http://osa1.net