The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

It sounds to me like you're getting into territory where ad-hoc answers 
on a mailing list won't be very effective.  An introduction to 
programming with dependent types in Coq (e.g., CPDT 
<http://adam.chlipala.net/cpdt/>) is probably worth reading.

On 04/05/2014 03:34 PM, Ömer Sinan Ağacan wrote:
> 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?
>