diff options
author | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
commit | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch) | |
tree | d88d05baf35b9b09a034233300f35a694f9fa6c2 /theories/Vectors/VectorDef.v | |
parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) |
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'theories/Vectors/VectorDef.v')
-rw-r--r-- | theories/Vectors/VectorDef.v | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 0fee50ff..30c0d4c0 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -40,17 +40,17 @@ Definition rectS {A} (P:forall {n}, t A (S n) -> Type) (rect: forall a {n} (v: t A (S n)), P v -> P (a :: v)) := fix rectS_fix {n} (v: t A (S n)) : P v := match v with - |nil => @id + |nil => fun devil => False_rect (@ID) devil |cons a 0 v => match v as vnn in t _ nn return match nn,vnn with |0,vm => P (a :: vm) - |S _,_ => ID + |S _,_ => _ end with |nil => bas a - |_ :: _ => @id + |_ :: _ => fun devil => False_rect (@ID) devil end |cons a (S nn') v => rect a v (rectS_fix v) end. @@ -66,11 +66,11 @@ match v1 as v1' in t _ n1 |[] => fun v2 => match v2 with |[] => bas - |_ :: _ => @id + |_ :: _ => fun devil => False_rect (@ID) devil end |h1 :: t1 => fun v2 => match v2 with - |[] => @id + |[] => fun devil => False_rect (@ID) devil |h2 :: t2 => fun t1' => rect (rect2_fix t1' t2) h1 h2 end t1 @@ -83,10 +83,10 @@ match v with end. (** A vector of length [S _] is [cons] *) -Definition caseS {A} (P : forall n, t A (S n) -> Type) - (H : forall h {n} t, @P n (h :: t)) {n} v : P n v := -match v with - |[] => @id (* Why needed ? *) +Definition caseS {A} (P : forall {n}, t A (S n) -> Type) + (H : forall h {n} t, @P n (h :: t)) {n} (v: t A (S n)) : P v := +match v as v' in t _ m return match m, v' with |0, _ => False -> True |S _, v0 => P v' end with + |[] => fun devil => False_rect _ devil (* subterm !!! *) |h :: t => H h t end. End SCHEMES. @@ -111,11 +111,12 @@ Fixpoint const {A} (a:A) (n:nat) := Computational behavior of this function should be the same as ocaml function. *) -Fixpoint nth {A} {m} (v' : t A m) (p : Fin.t m) {struct p} : A := +Definition nth {A} := +fix nth_fix {m} (v' : t A m) (p : Fin.t m) {struct v'} : A := match p in Fin.t m' return t A m' -> A with |Fin.F1 q => fun v => caseS (fun n v' => A) (fun h n t => h) v |Fin.FS q p' => fun v => (caseS (fun n v' => Fin.t n -> A) - (fun h n t p0 => nth t p0) v) p' + (fun h n t p0 => nth_fix t p0) v) p' end v'. (** An equivalent definition of [nth]. *) |