blob: eed7f0f3ffd2f9cec4efe023ecae72cc2eebed9d (
plain)
1
2
3
4
5
6
7
|
Require Import Vector.
Fail Program Fixpoint vector_rev {A : Type} {n1 n2 : nat} (v1 : Vector.t A n1) (v2 : Vector.t A n2) : Vector.t A (n1+n2) :=
match v1 with
| nil _ => v2
| cons _ e n' sv => vector_rev sv (cons A e n2 v2)
end.
|
