The Coq mailing list

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

Thanks for your answer! I tried using eq_nat_dec without using lemmas,
just to see how error will change and how does that help Coq inferring
stop = n, but it's still giving same error message:

  Fixpoint nth_triangle_aux {T : Type} (idx stop : nat) (tr :
triangle_t T idx) : Vector.t T stop :=
    if eq_nat_dec idx stop then
      match tr with triangle _ _ v _ => v end
    else
      match tr with triangle _ _ _ tr' => nth_triangle_aux (S idx) stop tr' 
end.

  Error:
  In environment
  nth_triangle_aux : forall (T : Type) (idx stop : nat),
                     triangle_t T idx -> Vector.t T stop
  T : Type
  idx : nat
  stop : nat
  tr : triangle_t T idx
  e : idx = stop
  T0 : Type
  n : nat
  v : Vector.t T0 n
  t : triangle_t T0 (S n)
  The term "v" has type "Vector.t T0 n" while it is expected to have type
   "Vector.t ?23 stop".

Is there anything else I need to do for telling Coq that stop = n?

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