diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean
index e94dab6075..822ba12fe8 100644
--- a/library/init/data/array/basic.lean
+++ b/library/init/data/array/basic.lean
@@ -1,133 +1,137 @@
 /-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Mario Carneiro
+Authors: Leonardo de Moura
 -/
 prelude
-import init.data.nat.basic init.data.fin.basic
+import init.data.nat.basic init.data.fin.basic init.data.usize init.data.repr init.function
 universes u v w
 
-/- In the VM, d_array is implemented a persistent array. -/
-structure d_array (n : nat) (α : fin n → Type u) :=
-(data : Π i : fin n, α i)
+/-
+The compiler has special support for arrays.
+They are implemented as a dynamic array.
+-/
 
-namespace d_array
-variables {n : nat} {α : fin n → Type u} {β : Type v}
+structure array (α : Type u) :=
+(sz   : nat)
+(data : fin sz → α)
 
-def nil {α} : d_array 0 α :=
-{data := λ ⟨x, h⟩, absurd h (nat.not_lt_zero x)}
+/- TODO: mark as builtin -/
+def mk_array {α : Type u} (n : nat) (v : α) : array α :=
+{ sz   := n,
+  data := λ _, v}
 
-/- has builtin VM implementation -/
-def read (a : d_array n α) (i : fin n) : α i :=
-a.data i
-
-/- has builtin VM implementation -/
-def write (a : d_array n α) (i : fin n) (v : α i) : d_array n α :=
-{data := λ j, if h : i = j then eq.rec_on h v else a.read j}
-
-def iterate_aux (a : d_array n α) (f : Π i : fin n, α i → β → β) : Π (i : nat), i ≤ n → β → β
-| 0     h b := b
-| (j+1) h b :=
-  let i : fin n := ⟨j, h⟩ in
-  f i (a.read i) (iterate_aux j (nat.le_of_lt h) b)
-
-/- has builtin VM implementation -/
-def iterate (a : d_array n α) (b : β) (f : Π i : fin n, α i → β → β) : β :=
-iterate_aux a f n (nat.le_refl _) b
-
-/- has builtin VM implementation -/
-def foreach (a : d_array n α) (f : Π i : fin n, α i → α i) : d_array n α :=
-iterate a a $ λ i v a', a'.write i (f i v)
-
-def map (f : Π i : fin n, α i → α i) (a : d_array n α) : d_array n α :=
-foreach a f
-
-def map₂ (f : Π i : fin n, α i → α i → α i) (a b : d_array n α) : d_array n α :=
-foreach b (λ i, f i (a.read i))
-
-def foldl (a : d_array n α) (b : β) (f : Π i : fin n, α i → β → β) : β :=
-iterate a b f
-
-def rev_iterate_aux (a : d_array n α) (f : Π i : fin n, α i → β → β) : Π (i : nat), i ≤ n → β → β
-| 0     h b := b
-| (j+1) h b :=
-  let i : fin n := ⟨j, h⟩ in
-  rev_iterate_aux j (nat.le_of_lt h) (f i (a.read i) b)
-
-def rev_iterate (a : d_array n α) (b : β) (f : Π i : fin n, α i → β → β) : β :=
-rev_iterate_aux a f n (nat.le_refl _) b
-
-end d_array
-
-def array (n : nat) (α : Type u) : Type u :=
-d_array n (λ _, α)
-
-/- has builtin VM implementation -/
-def mk_array {α} (n) (v : α) : array n α :=
-{data := λ _, v}
+theorem sz_mk_array_eq {α : Type u} (n : nat) (v : α) : (mk_array n v).sz = n :=
+rfl
 
 namespace array
-variables {n : nat} {α : Type u} {β : Type v}
+variables {α : Type u} {β : Type v}
 
-def nil {α} : array 0 α :=
-d_array.nil
+/- TODO: mark as builtin -/
+def nil : array α :=
+{ sz   := 0,
+  data := λ ⟨x, h⟩, absurd h (nat.not_lt_zero x) }
 
-def read (a : array n α) (i : fin n) : α :=
-d_array.read a i
+def empty (a : array α) : bool :=
+a.sz = 0
 
-def write (a : array n α) (i : fin n) (v : α) : array n α :=
-d_array.write a i v
+/- TODO: mark as builtin -/
+def read (a : array α) (i : fin a.sz) : α :=
+a.data i
 
-def iterate (a : array n α) (b : β) (f : fin n → α → β → β) : β :=
-d_array.iterate a b f
+/- TODO: mark as builtin -/
+def write (a : array α) (i : fin a.sz) (v : α) : array α :=
+{ sz   := a.sz,
+  data := λ j, if h : i = j then v else a.data j }
 
-def foreach (a : array n α) (f : fin n → α → α) : array n α :=
-iterate a a (λ i v a', a'.write i (f i v))
+theorem sz_write_eq (a : array α) (i : fin a.sz) (v : α) : (write a i v).sz = a.sz :=
+rfl
 
-def map (f : α → α) (a : array n α) : array n α :=
-foreach a (λ _, f)
+/- TODO: add builtin -/
+def read' [inhabited α] (a : array α) (i : nat) : α :=
+if h : i < a.sz then a.read ⟨i, h⟩ else default α
 
-def map₂ (f : α → α → α) (a b : array n α) : array n α :=
-foreach b (λ i, f (a.read i))
+/- TODO: add builtin -/
+def write' (a : array α) (i : nat) (v : α) : array α :=
+if h : i < a.sz then a.write ⟨i, h⟩ v else a
 
-def foldl (a : array n α) (b : β) (f : α → β → β) : β :=
+/- TODO: add builtin -/
+def uread [inhabited α] (a : array α) (i : usize) : α :=
+if h : i.val < a.sz then a.read ⟨i.val, h⟩ else default α
+
+/- TODO: add builtin -/
+def uwrite (a : array α) (i : usize) (v : α) : array α :=
+if h : i.val < a.sz then a.write ⟨i.val, h⟩ v else a
+
+/- TODO: mark as builtin -/
+def push (a : array α) (v : α) : array α :=
+{ sz   := nat.succ a.sz,
+  data := λ ⟨j, h₁⟩,
+    if h₂ : j = a.sz then v
+    else a.data ⟨j, nat.lt_of_le_of_ne (nat.le_of_lt_succ h₁) h₂⟩ }
+
+/- TODO: mark as builtin -/
+def pop (a : array α) : array α :=
+{ sz   := nat.pred a.sz,
+  data := λ ⟨j, h⟩, a.read ⟨j, nat.lt_of_lt_of_le h (nat.pred_le _)⟩ }
+
+private def iterate_aux (a : array α) (f : Π i : fin a.sz, α → β → β) : Π (i : nat), i ≤ a.sz → β → β
+| 0     h b := b
+| (j+1) h b :=
+  let i : fin a.sz := ⟨j, h⟩ in
+  f i (a.read i) (iterate_aux j (nat.le_of_lt h) b)
+
+/- TODO : mark as builtin -/
+def iterate (a : array α) (b : β) (f : Π i : fin a.sz, α → β → β) : β :=
+iterate_aux a f a.sz (nat.le_refl _) b
+
+def foldl (a : array α) (b : β) (f : α → β → β) : β :=
 iterate a b (λ _, f)
 
-def rev_list (a : array n α) : list α :=
-a.foldl [] (::)
+private def rev_iterate_aux (a : array α) (f : Π i : fin a.sz, α → β → β) : Π (i : nat), i ≤ a.sz → β → β
+| 0     h b := b
+| (j+1) h b :=
+  let i : fin a.sz := ⟨j, h⟩ in
+  rev_iterate_aux j (nat.le_of_lt h) (f i (a.read i) b)
 
-def rev_iterate (a : array n α) (b : β) (f : fin n → α → β → β) : β :=
-d_array.rev_iterate a b f
+/- TODO: mark as builtin -/
+def rev_iterate (a : array α) (b : β) (f : Π i : fin a.sz, α → β → β) : β :=
+rev_iterate_aux a f a.sz (nat.le_refl _) b
 
-def rev_foldl (a : array n α) (b : β) (f : α → β → β) : β :=
+def rev_foldl (a : array α) (b : β) (f : α → β → β) : β :=
 rev_iterate a b (λ _, f)
 
-def to_list (a : array n α) : list α :=
+def to_list (a : array α) : list α :=
 a.rev_foldl [] (::)
 
-theorem push_back_idx {j n} (h₁ : j < n + 1) (h₂ : j ≠ n) : j < n :=
-nat.lt_of_le_of_ne (nat.le_of_lt_succ h₁) h₂
+instance [has_repr α] : has_repr (array α) :=
+⟨repr ∘ to_list⟩
 
-/- has builtin VM implementation -/
-def push_back (a : array n α) (v : α) : array (n+1) α :=
-{data := λ ⟨j, h₁⟩, if h₂ : j = n then v else a.read ⟨j, push_back_idx h₁ h₂⟩}
+private def foreach_aux (a : array α) (f : Π i : fin a.sz, α → α) : { a' : array α // a'.sz = a.sz } :=
+iterate a ⟨a, rfl⟩ $ λ i v ⟨a', h⟩,
+  let i' : fin a'.sz := eq.rec_on h.symm i in
+  ⟨a'.write i' (f i v), (sz_write_eq a' i' (f i v)) ▸ h⟩
 
-theorem pop_back_idx {j n} (h : j < n) : j < n + 1 :=
-nat.lt.step h
+/- TODO : mark as builtin -/
+def foreach (a : array α) (f : Π i : fin a.sz, α → α) : array α :=
+(foreach_aux a f).val
 
-/- has builtin VM implementation -/
-def pop_back (a : array (n+1) α) : array n α :=
-{data := λ ⟨j, h⟩, a.read ⟨j, pop_back_idx h⟩}
+theorem sz_foreach_eq (a : array α) (f : Π i : fin a.sz, α → α) : (foreach a f).sz = a.sz :=
+(foreach_aux a f).property
 
-protected def mem (v : α) (a : array n α) : Prop :=
-∃ i : fin n, read a i = v
+def map (f : α → α) (a : array α) : array α :=
+foreach a (λ _, f)
 
-instance : has_mem α (array n α) := ⟨array.mem⟩
-
-def read' [inhabited β] (a : array n β) (i : nat) : β :=
-if h : i < n then a.read ⟨i,h⟩ else default β
-
-def write' (a : array n α) (i : nat) (v : α) : array n α :=
-if h : i < n then a.write ⟨i, h⟩ v else a
+def map₂ (f : α → α → α) (a b : array α) : array α :=
+if h : a.sz ≤ b.sz
+then foreach a (λ ⟨i, h'⟩, f (b.read ⟨i, nat.lt_of_lt_of_le h' h⟩))
+else foreach b (λ ⟨i, h'⟩, f (a.read ⟨i, nat.lt_trans h' (nat.gt_of_not_le h)⟩))
 
 end array
+
+def list.to_array_aux {α : Type u} : list α → array α → array α
+| []      r := r
+| (a::as) r := list.to_array_aux as (r.push a)
+
+def list.to_array {α : Type u} (l : list α) : array α :=
+l.to_array_aux array.nil
diff --git a/library/init/data/array/default.lean b/library/init/data/array/default.lean
index 05427fa21e..0760a52cf6 100644
--- a/library/init/data/array/default.lean
+++ b/library/init/data/array/default.lean
@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
 prelude
-import init.data.array.basic init.data.array.lemmas
+import init.data.array.basic
diff --git a/library/init/data/hashmap/basic.lean b/library/init/data/hashmap/basic.lean
index df7e4b71b9..ec9a78463e 100644
--- a/library/init/data/hashmap/basic.lean
+++ b/library/init/data/hashmap/basic.lean
@@ -7,24 +7,29 @@ prelude
 import init.data.array.basic init.data.list.basic init.data.option.basic
 universes u v w
 
-def bucket_array (α : Type u) (β : α → Type v) (n : nat) :=
-array n (list (Σ a, β a))
+def bucket_array (α : Type u) (β : α → Type v) :=
+{ b : array (list (Σ a, β a)) // b.sz > 0 }
+
+def bucket_array.write {α : Type u} {β : α → Type v} (data : bucket_array α β) (i : fin data.val.sz) (d : list (Σ a, β a)) : bucket_array α β :=
+⟨ data.val.write i d,
+  calc (data.val.write i d).sz = data.val.sz : array.sz_write_eq _ _ _
+                     ...       > 0           : data.property ⟩
 
 structure hashmap_imp (α : Type u) (β : α → Type v) :=
-(size nbuckets : nat)
-(nz_buckets    : nbuckets > 0)
-(buckets       : bucket_array α β nbuckets)
+(size       : nat)
+(buckets    : bucket_array α β)
 
 def mk_hashmap_imp {α : Type u} {β : α → Type v} (nbuckets := 8) : hashmap_imp α β :=
 let n := if nbuckets = 0 then 8 else nbuckets in
 { size       := 0,
-  nbuckets   := n,
-  nz_buckets := show (if nbuckets = 0 then 8 else nbuckets) > 0, from
-                match nbuckets with
-                | 0            := nat.zero_lt_succ _
-                | (nat.succ x) := nat.zero_lt_succ _
-                end,
-  buckets    := mk_array n [] }
+  buckets    :=
+  ⟨ mk_array n [],
+    calc (mk_array n []).sz = n                                    : sz_mk_array_eq _ _
+           ...              = if nbuckets = 0 then 8 else nbuckets : rfl
+           ...              > 0                                    :
+              match nbuckets with
+              | 0            := nat.zero_lt_succ _
+              | (nat.succ x) := nat.zero_lt_succ _ ⟩ }
 
 namespace hashmap_imp
 variables {α : Type u} {β : α → Type v}
@@ -32,12 +37,12 @@ variables {α : Type u} {β : α → Type v}
 def mk_idx {n : nat} (h : n > 0) (i : nat) : fin n :=
 ⟨i % n, nat.mod_lt _ h⟩
 
-def reinsert_aux (hash_fn : α → nat) {n : nat} (h : n > 0) (data : bucket_array α β n) (a : α) (b : β a) : bucket_array α β n :=
-let bidx := mk_idx h (hash_fn a) in
-data.write bidx (⟨a, b⟩ :: data.read bidx)
+def reinsert_aux (hash_fn : α → nat) (data : bucket_array α β) (a : α) (b : β a) : bucket_array α β :=
+let bidx := mk_idx data.property (hash_fn a) in
+data.write bidx (⟨a, b⟩ :: data.val.read bidx)
 
-def fold_buckets {δ : Type w} {n : nat} (data : bucket_array α β n) (d : δ) (f : δ → Π a, β a → δ) : δ :=
-data.foldl d (λ b d, b.foldl (λ r (p : Σ a, β a), f r p.1 p.2) d)
+def fold_buckets {δ : Type w} (data : bucket_array α β) (d : δ) (f : δ → Π a, β a → δ) : δ :=
+data.val.foldl d (λ b d, b.foldl (λ r (p : Σ a, β a), f r p.1 p.2) d)
 
 def find_aux [decidable_eq α] (a : α) : list (Σ a, β a) → option (β a)
 | []          := none
@@ -49,9 +54,8 @@ def contains_aux [decidable_eq α] (a : α) (l : list (Σ a, β a)) : bool :=
 
 def find [decidable_eq α] (hash_fn : α → nat) (m : hashmap_imp α β) (a : α) : option (β a) :=
 match m with
-| ⟨_, nbuckets, nz, buckets⟩ :=
+| ⟨_, buckets, nz⟩ :=
   find_aux a (buckets.read (mk_idx nz (hash_fn a)))
-end
 
 def fold {δ : Type w} (m : hashmap_imp α β) (d : δ) (f : δ → Π a, β a → δ) : δ :=
 fold_buckets m.buckets d f
@@ -66,31 +70,28 @@ def erase_aux [decidable_eq α] (a : α) : list (Σ a, β a) → list (Σ a, β
 
 def insert [decidable_eq α] (hash_fn : α → nat) (m : hashmap_imp α β) (a : α) (b : β a) : hashmap_imp α β :=
 match m with
-| ⟨size, nbuckets, nz, buckets⟩ :=
-  let bidx := mk_idx nz (hash_fn a) in
-  let bkt  := buckets.read bidx in
+| ⟨size, buckets⟩ :=
+  let bidx := mk_idx buckets.property (hash_fn a) in
+  let bkt  := buckets.val.read bidx in
   if contains_aux a bkt
-  then ⟨size, nbuckets, nz, buckets.write bidx (replace_aux a b bkt)⟩
+  then ⟨size, buckets.write bidx (replace_aux a b bkt)⟩
   else let size'    := size + 1 in
        let buckets' := buckets.write bidx (⟨a, b⟩::bkt) in
-       if size' <= nbuckets
-       then ⟨size', nbuckets, nz, buckets'⟩
-       else let nbuckets' := nbuckets * 2 in
-            let nz' : nbuckets' > 0 := nat.mul_pos nz (nat.zero_lt_bit0 nat.one_ne_zero) in
-            ⟨size', nbuckets', nz',
-            fold_buckets buckets' (mk_array nbuckets' []) $
-               λ r a b, reinsert_aux hash_fn nz' r a b⟩
-end
+       if size' <= buckets.val.sz
+       then ⟨size', buckets'⟩
+       else let nbuckets' := buckets.val.sz * 2 in
+            let nz' : nbuckets' > 0 := nat.mul_pos buckets.property (nat.zero_lt_bit0 nat.one_ne_zero) in
+            ⟨ size',
+              fold_buckets buckets' ⟨mk_array nbuckets' [], nz'⟩ (reinsert_aux hash_fn) ⟩
 
 def erase [decidable_eq α] (hash_fn : α → nat) (m : hashmap_imp α β) (a : α) : hashmap_imp α β :=
 match m with
-| ⟨size, nbuckets, nz, buckets⟩ :=
-  let bidx : fin nbuckets := ⟨hash_fn a % nbuckets, nat.mod_lt _ nz⟩ in
-  let bkt                 := buckets.read bidx in
+| ⟨ size, buckets ⟩ :=
+  let bidx := mk_idx buckets.property (hash_fn a) in
+  let bkt  := buckets.val.read bidx in
   if contains_aux a bkt
-  then ⟨size - 1, nbuckets, nz, buckets.write bidx $ erase_aux a bkt⟩
+  then ⟨size - 1, buckets.write bidx $ erase_aux a bkt⟩
   else m
-end
 
 inductive well_formed [decidable_eq α] (hash_fn : α → nat) : hashmap_imp α β → Prop
 | mk_wff     : ∀ n,                     well_formed (mk_hashmap_imp n)
diff --git a/src/library/vm/vm_array.cpp b/src/library/vm/vm_array.cpp
index 3c7a36b8be..72247d2ef1 100644
--- a/src/library/vm/vm_array.cpp
+++ b/src/library/vm/vm_array.cpp
@@ -63,16 +63,20 @@ vm_obj to_obj(parray<vm_obj> const & a) {
     return mk_vm_external(new vm_array(a));
 }
 
-vm_obj d_array_read(vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj const & i) {
-    /* TODO(Leo): handle case where n is too big */
+vm_obj array_sz(vm_obj const &, vm_obj const & a) {
+    return mk_vm_nat(to_array(a).size());
+}
+
+vm_obj array_read(vm_obj const &, vm_obj const & a, vm_obj const & i) {
+    /* TODO(Leo): handle case where i is too big */
     unsigned idx = force_to_unsigned(i);
     lean_vm_check(idx < to_array(a).size());
     parray<vm_obj> const & _a = to_array(a);
     return _a[idx];
 }
 
-vm_obj d_array_write(vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj const & i, vm_obj const & v) {
-    /* TODO(Leo): handle case where n is too big */
+vm_obj array_write(vm_obj const &, vm_obj const & a, vm_obj const & i, vm_obj const & v) {
+    /* TODO(Leo): handle case where i is too big */
     unsigned idx = force_to_unsigned(i);
     parray<vm_obj> const & p = to_array(a);
     lean_vm_check(idx < p.size());
@@ -86,7 +90,7 @@ vm_obj d_array_write(vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj co
     }
 }
 
-vm_obj array_push_back(vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj const & v) {
+vm_obj array_push(vm_obj const &, vm_obj const & a, vm_obj const & v) {
     parray<vm_obj> const & p = to_array(a);
     if (a.raw()->get_rc() == 1) {
         const_cast<parray<vm_obj> &>(p).push_back(v);
@@ -98,7 +102,7 @@ vm_obj array_push_back(vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj
     }
 }
 
-vm_obj array_pop_back(vm_obj const &, vm_obj const &, vm_obj const & a) {
+vm_obj array_pop(vm_obj const &, vm_obj const & a) {
     parray<vm_obj> const & p = to_array(a);
     if (a.raw()->get_rc() == 1) {
         const_cast<parray<vm_obj> &>(p).pop_back();
@@ -117,7 +121,7 @@ vm_obj mk_array(vm_obj const & /* alpha */, vm_obj const & n, vm_obj const & v)
     return to_obj(a);
 }
 
-vm_obj d_array_mk(vm_obj const & n, vm_obj const & /* alpha */, vm_obj const & fn) {
+vm_obj array_mk(vm_obj const & /* alpha */, vm_obj const & n, vm_obj const & fn) {
     /* TODO(Leo): handle case where n is too big */
     unsigned _n = force_to_unsigned(n);
     parray<vm_obj> a;
@@ -127,10 +131,10 @@ vm_obj d_array_mk(vm_obj const & n, vm_obj const & /* alpha */, vm_obj const & f
     return to_obj(a);
 }
 
-vm_obj d_array_foreach(vm_obj const & n, vm_obj const & /* alpha */, vm_obj const & a, vm_obj const & fn) {
+vm_obj array_foreach(vm_obj const & /* alpha */, vm_obj const & a, vm_obj const & fn) {
     /* TODO(Leo): handle case where n is too big */
-    unsigned _n = force_to_unsigned(n);
     parray<vm_obj> const & p = to_array(a);
+    unsigned _n = p.size();
     if (a.raw()->get_rc() == 1) {
         parray<vm_obj> & _p = const_cast<parray<vm_obj> &>(p);
         for (unsigned i = 0; i < _n; i++)
@@ -145,11 +149,10 @@ vm_obj d_array_foreach(vm_obj const & n, vm_obj const & /* alpha */, vm_obj cons
     }
 }
 
-vm_obj d_array_iterate(vm_obj const & n, vm_obj const & /* alpha */, vm_obj const & /* beta */,
-                       vm_obj const & a, vm_obj const & b, vm_obj const & fn) {
-    /* TODO(Leo): handle case where n is too big */
-    unsigned _n = force_to_unsigned(n);
+vm_obj array_iterate(vm_obj const & /* alpha */, vm_obj const & /* beta */,
+                     vm_obj const & a, vm_obj const & b, vm_obj const & fn) {
     parray<vm_obj> const & p = to_array(a);
+    unsigned _n              = p.size();
     vm_obj r = b;
     for (unsigned i = 0; i < _n; i++)
         r = invoke(fn, mk_vm_nat(i), p[i], r);
@@ -158,30 +161,32 @@ vm_obj d_array_iterate(vm_obj const & n, vm_obj const & /* alpha */, vm_obj cons
 
 static unsigned g_array_read_idx = -1;
 
-unsigned d_array_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
-    vm_obj d[3] = {o, mk_vm_unit(), mk_vm_unit()};
-    vm_obj fn = mk_vm_closure(g_array_read_idx, 3, d);
+unsigned array_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
+    vm_obj d[2] = {o, mk_vm_unit()};
+    vm_obj fn = mk_vm_closure(g_array_read_idx, 2, d);
+    data.push_back(mk_vm_nat(to_array(o).size()));
     data.push_back(fn);
     return 0;
 }
 
 void initialize_vm_array() {
-    DECLARE_VM_BUILTIN(name({"d_array", "mk"}),             d_array_mk);
-    DECLARE_VM_BUILTIN(name({"mk_array"}),                  mk_array);
-    DECLARE_VM_BUILTIN(name({"d_array", "data"}),           d_array_read);
-    DECLARE_VM_BUILTIN(name({"d_array", "read"}),           d_array_read);
-    DECLARE_VM_BUILTIN(name({"d_array", "write"}),          d_array_write);
-    DECLARE_VM_BUILTIN(name({"array", "push_back"}),        array_push_back);
-    DECLARE_VM_BUILTIN(name({"array", "pop_back"}),         array_pop_back);
-    DECLARE_VM_BUILTIN(name({"d_array", "foreach"}),        d_array_foreach);
-    DECLARE_VM_BUILTIN(name({"d_array", "iterate"}),        d_array_iterate);
-    DECLARE_VM_CASES_BUILTIN(name({"d_array", "cases_on"}), d_array_cases_on);
+    DECLARE_VM_BUILTIN(name({"array", "mk"}),             array_mk);
+    DECLARE_VM_BUILTIN(name({"mk_array"}),                mk_array);
+    DECLARE_VM_BUILTIN(name({"array", "sz"}),             array_sz);
+    DECLARE_VM_BUILTIN(name({"array", "data"}),           array_read);
+    DECLARE_VM_BUILTIN(name({"array", "read"}),           array_read);
+    DECLARE_VM_BUILTIN(name({"array", "write"}),          array_write);
+    DECLARE_VM_BUILTIN(name({"array", "push"}),           array_push);
+    DECLARE_VM_BUILTIN(name({"array", "pop"}),            array_pop);
+    DECLARE_VM_BUILTIN(name({"array", "foreach"}),        array_foreach);
+    DECLARE_VM_BUILTIN(name({"array", "iterate"}),        array_iterate);
+    DECLARE_VM_CASES_BUILTIN(name({"array", "cases_on"}), array_cases_on);
 }
 
 void finalize_vm_array() {
 }
 
 void initialize_vm_array_builtin_idxs() {
-    g_array_read_idx = *get_vm_builtin_idx(name({"d_array", "read"}));
+    g_array_read_idx = *get_vm_builtin_idx(name({"array", "read"}));
 }
 }
diff --git a/tests/lean/run/array1.lean b/tests/lean/run/array1.lean
new file mode 100644
index 0000000000..f0d80552f0
--- /dev/null
+++ b/tests/lean/run/array1.lean
@@ -0,0 +1,27 @@
+#check @array.mk
+
+#eval mk_array 4 1
+
+def v : array nat := @array.mk nat 10 (λ ⟨i, _⟩, i)
+
+#eval array.map (+10) v
+
+def w : array nat :=
+(mk_array 9 1).push 3
+
+def f : fin w.sz → nat :=
+array.cases_on w (λ _ f, f)
+
+#eval f ⟨1, sorry⟩
+#eval f ⟨9, sorry⟩
+
+#eval (((mk_array 1 1).push 2).push 3).foldl 0 (+)
+
+def array_sum (a : array nat) : nat :=
+a.foldl 0 (+)
+
+#eval array_sum (mk_array 10 1)
+
+#eval (mk_array 10 1).data ⟨1, dec_trivial⟩ + 20
+#eval (mk_array 10 1).data ⟨2, dec_trivial⟩
+#eval (mk_array 10 3).data ⟨2, dec_trivial⟩