aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/ImplicitArguments.v
blob: e7795733f69c172cb9c0ceea7c047c870201c77b (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
Inductive vector {A : Type} : nat -> Type :=
| vnil : vector 0
| vcons : A -> forall {n'}, vector n' -> vector (S n').

Require Import Coq.Program.Program.

Program Definition head {A : Type} {n : nat} (v : vector A (S n)) : vector A n :=
  match v with
    | vnil => !
    | vcons a n' v' => v'
  end.

Fixpoint app {A : Type} {n m : nat} (v : vector A n) (w : vector A m) : vector A (n + m) :=
  match v in vector _ n return vector A (n + m) with
    | vnil => w
    | vcons a n' v' => vcons a (app v' w)
  end.