diff options
Diffstat (limited to 'theories/Vectors/VectorDef.v')
| -rw-r--r-- | theories/Vectors/VectorDef.v | 22 |
1 files changed, 16 insertions, 6 deletions
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 1f8b76cb..f6f3cafa 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Definitions of Vectors and functions to use them @@ -147,6 +149,16 @@ Definition shiftrepeat {A} := @rectS _ (fun n _ => t A (S (S n))) (fun h => h :: h :: []) (fun h _ _ H => h :: H). Global Arguments shiftrepeat {A} {n} v. +(** Take first [p] elements of a vector *) +Fixpoint take {A} {n} (p:nat) (le:p <= n) (v:t A n) : t A p := + match p as p return p <= n -> t A p with + | 0 => fun _ => [] + | S p' => match v in t _ n return S p' <= n -> t A (S p') with + | []=> fun le => False_rect _ (Nat.nle_succ_0 p' le) + | x::xs => fun le => x::take p' (le_S_n p' _ le) xs + end + end le. + (** Remove [p] last elements of a vector *) Lemma trunc : forall {A} {n} (p:nat), n > p -> t A n -> t A (n - p). @@ -295,12 +307,10 @@ End VECTORLIST. Module VectorNotations. Delimit Scope vector_scope with vector. Notation "[ ]" := [] (format "[ ]") : vector_scope. -Notation "[]" := [] (compat "8.5") : vector_scope. Notation "h :: t" := (h :: t) (at level 60, right associativity) : vector_scope. Notation "[ x ]" := (x :: []) : vector_scope. Notation "[ x ; y ; .. ; z ]" := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope. -Notation "[ x ; .. ; y ]" := (cons _ x _ .. (cons _ y _ (nil _)) ..) (compat "8.4") : vector_scope. Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope. Open Scope vector_scope. End VectorNotations. |