The Coq mailing list

[rcp AT Cs.Nott.AC.UK]

> I'm stuck again in trying to write some dependent code. I want to index a
> vector:
>
>   Section vectors.
>   
>   Variable (A : Set).
>   
>   Inductive vec : nat -> Set :=
>     | vnil : vec 0
>     | vcons : forall n, A -> vec n -> vec (S n).
>   
>   Inductive fin : nat -> Set :=
>     | finz : fin 1
>     | fins : forall n, fin n -> fin (S n). 
>   
>   Fixpoint vind n (i : fin n) {struct i} : vec n -> A :=
>     match i in fin n return vec n -> A with
>     | finz => fun v => 
>         match v in vec m return (match m with 0 => True | S _ => A end) 
> with
>         | vnil => I
>         | vcons _ x _ => x
>         end
>     | fins m j => fun v =>
>         match v in vec m return (match m with 0 => True | S _ => A end) 
> with
>         | vnil => I
>         | vcons m' _ xs => vind m j xs (* wrong *)
>         end
>     end.
vec A n is isomorphic to (Fin n -> A). If you intend to work with both vec 
and Fin, you should define this isomorphism, and you'd then be able to get 
the function you want rather easily.

Best,

RP> 


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.