blob: f702aa62f1f41535e3726bd263b2430ebad689e7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
Inductive vector {A : Type} : nat -> Type :=
| vnil : vector 0
| vcons : A -> forall {n'}, vector n' -> vector (S n').
Implicit Arguments vector [].
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 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 v' => vcons a (app v' w)
end.
(* Test sharing information between different hypotheses *)
Parameters (a:_) (b:a=0).
|
