diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2015-02-11 19:33:46 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2015-02-11 19:33:46 +0100 |
| commit | e191cc298e684fa4231c97abf4f89ab0f1b3a42c (patch) | |
| tree | e0cc87568181508fa0799de0aed5957435d715b2 | |
| parent | 4edc539b83bddb2483b9c8ba1cf82fc81c717abd (diff) | |
| download | smtcoq-e191cc298e684fa4231c97abf4f89ab0f1b3a42c.tar.gz smtcoq-e191cc298e684fa4231c97abf4f89ab0f1b3a42c.zip | |
More efficient initialization of an array
| -rw-r--r-- | src/versions/standard/Array/PArray_standard.v | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/src/versions/standard/Array/PArray_standard.v b/src/versions/standard/Array/PArray_standard.v index 069c159..eb43cb0 100644 --- a/src/versions/standard/Array/PArray_standard.v +++ b/src/versions/standard/Array/PArray_standard.v @@ -31,16 +31,12 @@ Local Open Scope int63_scope. Module Map := FMapAVL.Make(IntOrderedType). +(* An array is represented as a tuple of a finite map, the default + element, and the length *) Definition array (A:Type) : Type := (Map.t A * A * int)%type. -Definition make {A:Type} (l:int) (d:A) : array A := - let r := - if l == 0 then - Map.empty A - else - foldi (fun j m => Map.add j d m) 0 (l-1) (Map.empty A) in - (r, d, l). +Definition make {A:Type} (l:int) (d:A) : array A := (Map.empty A, d, l). Definition get {A:Type} (t:array A) (i:int) : A := let (td,_) := t in |