chore: update constants

leanprover · Sep 9, 2024 · 21905bc · 21905bc
1 parent 172c1ac
commit 21905bc
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 7 deletions.
diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp
@@ -215,7 +215,7 @@ class erase_irrelevant_fn {
         expr minor       = visit_minor(args[3]);
         lean_always_assert(is_lambda(minor));
         return
-            ::lean::mk_let(next_name(), mk_enf_object_type(), mk_app(mk_constant(get_array_data_name()), mk_enf_neutral(), major),
+            ::lean::mk_let(next_name(), mk_enf_object_type(), mk_app(mk_constant(get_array_to_list_name()), mk_enf_neutral(), major),
                            binding_body(minor));
     }
 

diff --git a/src/library/constants.cpp b/src/library/constants.cpp
@@ -12,7 +12,7 @@ name const * g_and_rec = nullptr;
 name const * g_and_cases_on = nullptr;
 name const * g_array = nullptr;
 name const * g_array_sz = nullptr;
-name const * g_array_data = nullptr;
+name const * g_array_to_list = nullptr;
 name const * g_auto_param = nullptr;
 name const * g_bit0 = nullptr;
 name const * g_bit1 = nullptr;
@@ -127,8 +127,8 @@ void initialize_constants() {
     mark_persistent(g_array->raw());
     g_array_sz = new name{"Array", "sz"};
     mark_persistent(g_array_sz->raw());
-    g_array_data = new name{"Array", "data"};
-    mark_persistent(g_array_data->raw());
+    g_array_to_list = new name{"Array", "toList"};
+    mark_persistent(g_array_to_list->raw());
     g_auto_param = new name{"autoParam"};
     mark_persistent(g_auto_param->raw());
     g_bit0 = new name{"bit0"};
@@ -330,7 +330,7 @@ void finalize_constants() {
     delete g_and_cases_on;
     delete g_array;
     delete g_array_sz;
-    delete g_array_data;
+    delete g_array_to_list;
     delete g_auto_param;
     delete g_bit0;
     delete g_bit1;
@@ -436,7 +436,7 @@ name const & get_and_rec_name() { return *g_and_rec; }
 name const & get_and_cases_on_name() { return *g_and_cases_on; }
 name const & get_array_name() { return *g_array; }
 name const & get_array_sz_name() { return *g_array_sz; }
-name const & get_array_data_name() { return *g_array_data; }
+name const & get_array_to_list_name() { return *g_array_to_list; }
 name const & get_auto_param_name() { return *g_auto_param; }
 name const & get_bit0_name() { return *g_bit0; }
 name const & get_bit1_name() { return *g_bit1; }

diff --git a/src/library/constants.h b/src/library/constants.h
@@ -14,7 +14,7 @@ name const & get_and_rec_name();
 name const & get_and_cases_on_name();
 name const & get_array_name();
 name const & get_array_sz_name();
-name const & get_array_data_name();
+name const & get_array_to_list_name();
 name const & get_auto_param_name();
 name const & get_bit0_name();
 name const & get_bit1_name();