The Coq mailing list

[dimitrisg7 <dvekris AT hotmail.com>]

Hello to everyone!

Is it possible to get the nth object (of type rel (nth ...) (nth ...)) in
the following inductive definition (I do not think that I can) or should I
make some changes in my definitions?

Section testing.
Set Implicit Arguments.

Variable A : Type.
Variable dA : A.
Variable B : Type.
Variable dB : B.
Variable rel: A -> B -> Type.

Inductive test : list A -> list B -> Type :=
| constr1 : test nil nil
| constr2 : forall a b al bl, rel a b -> test al bl -> test (a::al)(b::bl).

Definition nth_dep n al bl (t : test al bl) : rel(nth n al dA)(nth n bl dB). 
Proof.
(* get nth object *)
Admitted.

End testing.

-----
Never say never.
-- 
View this message in context: 
http://www.nabble.com/Nth---dependent-types.-tp23241301p23241301.html
Sent from the Coq mailing list archive at Nabble.com.