diff --git a/src/library/compiler/simp_inductive.cpp b/src/library/compiler/simp_inductive.cpp
index 98ec091ac1..78951ad5bd 100644
--- a/src/library/compiler/simp_inductive.cpp
+++ b/src/library/compiler/simp_inductive.cpp
@@ -203,12 +203,16 @@ class simp_inductive_fn : public compiler_step_visitor {
         }
     }
 
+    expr visit_default(name const & fn, buffer<expr> const & args) {
+        buffer<expr> new_args;
+        for (expr const & arg : args)
+            new_args.push_back(visit(arg));
+        return mk_app(mk_constant(fn), new_args);
+    }
+
     expr visit_constructor(name const & fn, buffer<expr> const & args) {
         if (is_vm_builtin_function(fn)) {
-            buffer<expr> new_args;
-            for (expr const & arg : args)
-                new_args.push_back(visit(arg));
-            return mk_app(mk_constant(fn), new_args);
+            return visit_default(fn, args);
         } else {
             /* The following invariant should hold since erase_irrelevant rejected code
                where it doesn't hold. */
@@ -235,30 +239,34 @@ class simp_inductive_fn : public compiler_step_visitor {
     }
 
     expr visit_projection(name const & fn, buffer<expr> const & args) {
-        projection_info const & info = *get_projection_info(env(), fn);
-        expr major = visit(args[info.m_nparams]);
-        buffer<bool> rel_fields;
-        name I_name = *inductive::is_intro_rule(env(), info.m_constructor);
-        get_constructor_info(info.m_constructor, rel_fields);
-        lean_assert(info.m_i < rel_fields.size());
-        lean_assert(rel_fields[info.m_i]); /* We already erased irrelevant information */
-        /* Adjust projection index by ignoring irrelevant fields */
-        unsigned j = 0;
-        for (unsigned i = 0; i < info.m_i; i++) {
-            if (rel_fields[i])
-                j++;
-        }
-        expr r;
-        if (has_trivial_structure(I_name, rel_fields)) {
-            lean_assert(j == 0);
-            r = major;
+        if (is_vm_builtin_function(fn)) {
+            return visit_default(fn, args);
         } else {
-            r = mk_app(mk_proj(j), major);
+            projection_info const & info = *get_projection_info(env(), fn);
+            expr major = visit(args[info.m_nparams]);
+            buffer<bool> rel_fields;
+            name I_name = *inductive::is_intro_rule(env(), info.m_constructor);
+            get_constructor_info(info.m_constructor, rel_fields);
+            lean_assert(info.m_i < rel_fields.size());
+            lean_assert(rel_fields[info.m_i]); /* We already erased irrelevant information */
+            /* Adjust projection index by ignoring irrelevant fields */
+            unsigned j = 0;
+            for (unsigned i = 0; i < info.m_i; i++) {
+                if (rel_fields[i])
+                    j++;
+            }
+            expr r;
+            if (has_trivial_structure(I_name, rel_fields)) {
+                lean_assert(j == 0);
+                r = major;
+            } else {
+                r = mk_app(mk_proj(j), major);
+            }
+            /* Add additional arguments */
+            for (unsigned i = info.m_nparams + 1; i < args.size(); i++)
+                r = mk_app(r, visit(args[i]));
+            return r;
         }
-        /* Add additional arguments */
-        for (unsigned i = info.m_nparams + 1; i < args.size(); i++)
-            r = mk_app(r, visit(args[i]));
-        return r;
     }
 
     virtual expr visit_app(expr const & e) override {
diff --git a/src/library/vm/vm_array.cpp b/src/library/vm/vm_array.cpp
index eb46a7421e..deba59bae1 100644
--- a/src/library/vm/vm_array.cpp
+++ b/src/library/vm/vm_array.cpp
@@ -168,6 +168,7 @@ unsigned array_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
 void initialize_vm_array() {
     DECLARE_VM_BUILTIN(name({"array", "mk"}),               array_mk);
     DECLARE_VM_BUILTIN(name({"mk_array"}),                  mk_array);
+    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_back"}),        array_push_back);
diff --git a/tests/lean/run/array1.lean b/tests/lean/run/array1.lean
index b17d97a672..74ccb3423e 100644
--- a/tests/lean/run/array1.lean
+++ b/tests/lean/run/array1.lean
@@ -23,4 +23,6 @@ a^.foldl 0 (+)
 
 #eval array_sum (mk_array 10 1)
 
-#eval (mk_array 10 1)^.data ⟨1, dec_trivial⟩
+#eval (mk_array 10 1)^.data ⟨1, dec_trivial⟩ + 20
+#eval (mk_array 10 1)^.data 2
+#eval (mk_array 10 3)^.data 2