feat(library/init/lean/eqncompiler): register [matchPattern] attribute using new attribute manager

library/init/lean/default.lean

@@ -14,3 +14,4 @@ import init.lean.evalconst
 import init.lean.parser
 import init.lean.reducibilityattrs
 import init.lean.elaborator
+import init.lean.eqncompiler

library/init/lean/eqncompiler/default.lean

@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.lean.eqncompiler.matchpattern

library/init/lean/eqncompiler/matchpattern.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.lean.attributes
+
+namespace Lean
+namespace EqnCompiler
+
+def mkMatchPatternAttr : IO TagAttribute :=
+registerTagAttribute `matchPattern "mark that a definition can be used in a pattern (remark: the dependent pattern matching compiler will unfold the definition)"
+
+@[init mkMatchPatternAttr]
+constant matchPatternAttr : TagAttribute := default _
+
+@[export lean.has_match_pattern_attribute_core]
+def hasMatchPatternAttribute (env : Environment) (n : Name) : Bool :=
+matchPatternAttr.hasTag env n
+
+end EqnCompiler
+end Lean

src/library/init_module.cpp

@@ -32,7 +32,6 @@ Author: Leonardo de Moura
 #include "library/attribute_manager.h"
 #include "library/app_builder.h"
 #include "library/fun_info.h"
-#include "library/pattern_attribute.h"
 #include "library/check.h"
 #include "library/parray.h"
 #include "library/profiling.h"
@@ -91,7 +90,6 @@ void initialize_library_module() {
     initialize_fun_info();
     initialize_abstract_context_cache();
     initialize_type_context();
-    initialize_pattern_attribute();
     initialize_check();
     initialize_parray();
     initialize_time_task();
@@ -101,7 +99,6 @@ void finalize_library_module() {
     finalize_time_task();
     finalize_parray();
     finalize_check();
-    finalize_pattern_attribute();
     finalize_type_context();
     finalize_abstract_context_cache();
     finalize_fun_info();

src/library/pattern_attribute.cpp

@@ -4,30 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "library/attribute_manager.h"
+#include "kernel/environment.h"
 
 namespace lean {
-static name * g_pattern_attr = nullptr;
-
-static basic_attribute const & get_pattern_attribute() {
-    return static_cast<basic_attribute const &>(get_system_attribute(*g_pattern_attr));
-}
+uint8 has_match_pattern_attribute_core(object*, object*);
 
 bool has_pattern_attribute(environment const & env, name const & d) {
-    return has_attribute(env, *g_pattern_attr, d);
-}
-
-environment set_pattern_attribute(environment const & env, name const & n) {
-    return get_pattern_attribute().set(env, get_dummy_ios(), n, LEAN_DEFAULT_PRIORITY, true);
-}
-
-void initialize_pattern_attribute() {
-    g_pattern_attr = new name({"matchPattern"});
-    register_system_attribute(basic_attribute(*g_pattern_attr, "mark that a definition can be used in a pattern"
-                                              "(remark: the dependent pattern matching compiler will unfold the definition)"));
-}
-
-void finalize_pattern_attribute() {
-    delete g_pattern_attr;
+    return has_match_pattern_attribute_core(env.to_obj_arg(), d.to_obj_arg());
 }
 }

src/library/pattern_attribute.h

@@ -8,7 +8,4 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 namespace lean {
 bool has_pattern_attribute(environment const & env, name const & d);
-environment set_pattern_attribute(environment const & env, name const & d);
-void initialize_pattern_attribute();
-void finalize_pattern_attribute();
 }

src/stage0/CMakeLists.txt

@@ -1 +1 @@
-add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/conditional.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/binsearch.cpp ./init/data/array/default.cpp ./init/data/array/qsort.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/bytearray/basic.cpp ./init/data/bytearray/default.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/persistentarray/basic.cpp ./init/data/persistentarray/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/attributes.cpp ./init/lean/compiler/closedtermcache.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/exportattr.cpp ./init/lean/compiler/externattr.cpp ./init/lean/compiler/initattr.cpp ./init/lean/compiler/inlineattrs.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/borrow.cpp ./init/lean/compiler/ir/boxing.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/compilerm.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/emitcpp.cpp ./init/lean/compiler/ir/emitutil.cpp ./init/lean/compiler/ir/expandresetreuse.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/rc.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/namemangling.cpp ./init/lean/compiler/specializeattrs.cpp ./init/lean/compiler/util.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/elaborator/default.cpp ./init/lean/elaborator/elabstrategyattrs.cpp ./init/lean/environment.cpp ./init/lean/evalconst.cpp ./init/lean/expr.cpp ./init/lean/format.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/modifiers.cpp ./init/lean/name.cpp ./init/lean/options.cpp ./init/lean/parser/default.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/parser.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/projfns.cpp ./init/lean/reducibilityattrs.cpp ./init/lean/runtime.cpp ./init/lean/smap.cpp ./init/lean/syntax.cpp ./init/lean/toexpr.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp)
+add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/conditional.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/binsearch.cpp ./init/data/array/default.cpp ./init/data/array/qsort.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/bytearray/basic.cpp ./init/data/bytearray/default.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/persistentarray/basic.cpp ./init/data/persistentarray/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/attributes.cpp ./init/lean/compiler/closedtermcache.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/exportattr.cpp ./init/lean/compiler/externattr.cpp ./init/lean/compiler/initattr.cpp ./init/lean/compiler/inlineattrs.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/borrow.cpp ./init/lean/compiler/ir/boxing.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/compilerm.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/emitcpp.cpp ./init/lean/compiler/ir/emitutil.cpp ./init/lean/compiler/ir/expandresetreuse.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/rc.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/namemangling.cpp ./init/lean/compiler/specializeattrs.cpp ./init/lean/compiler/util.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/elaborator/default.cpp ./init/lean/elaborator/elabstrategyattrs.cpp ./init/lean/environment.cpp ./init/lean/eqncompiler/default.cpp ./init/lean/eqncompiler/matchpattern.cpp ./init/lean/evalconst.cpp ./init/lean/expr.cpp ./init/lean/format.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/modifiers.cpp ./init/lean/name.cpp ./init/lean/options.cpp ./init/lean/parser/default.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/parser.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/projfns.cpp ./init/lean/reducibilityattrs.cpp ./init/lean/runtime.cpp ./init/lean/smap.cpp ./init/lean/syntax.cpp ./init/lean/toexpr.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp)

src/stage0/init/lean/default.cpp

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: init.lean.default
-// Imports: init.lean.compiler.default init.lean.environment init.lean.modifiers init.lean.projfns init.lean.runtime init.lean.attributes init.lean.evalconst init.lean.parser.default init.lean.reducibilityattrs init.lean.elaborator.default
+// Imports: init.lean.compiler.default init.lean.environment init.lean.modifiers init.lean.projfns init.lean.runtime init.lean.attributes init.lean.evalconst init.lean.parser.default init.lean.reducibilityattrs init.lean.elaborator.default init.lean.eqncompiler.default
 #include "runtime/object.h"
 #include "runtime/apply.h"
 typedef lean::object obj;    typedef lean::usize  usize;
@@ -24,6 +24,7 @@ obj* initialize_init_lean_evalconst(obj*);
 obj* initialize_init_lean_parser_default(obj*);
 obj* initialize_init_lean_reducibilityattrs(obj*);
 obj* initialize_init_lean_elaborator_default(obj*);
+obj* initialize_init_lean_eqncompiler_default(obj*);
 static bool _G_initialized = false;
 obj* initialize_init_lean_default(obj* w) {
 if (_G_initialized) return w;
@@ -49,5 +50,7 @@ w = initialize_init_lean_reducibilityattrs(w);
 if (io_result_is_error(w)) return w;
 w = initialize_init_lean_elaborator_default(w);
 if (io_result_is_error(w)) return w;
+w = initialize_init_lean_eqncompiler_default(w);
+if (io_result_is_error(w)) return w;
 return w;
 }

src/stage0/init/lean/eqncompiler/default.cpp

@@ -0,0 +1,26 @@
+// Lean compiler output
+// Module: init.lean.eqncompiler.default
+// Imports: init.lean.eqncompiler.matchpattern
+#include "runtime/object.h"
+#include "runtime/apply.h"
+typedef lean::object obj;    typedef lean::usize  usize;
+typedef lean::uint8  uint8;  typedef lean::uint16 uint16;
+typedef lean::uint32 uint32; typedef lean::uint64 uint64;
+#if defined(__clang__)
+#pragma clang diagnostic ignored "-Wunused-parameter"
+#pragma clang diagnostic ignored "-Wunused-label"
+#elif defined(__GNUC__) && !defined(__CLANG__)
+#pragma GCC diagnostic ignored "-Wunused-parameter"
+#pragma GCC diagnostic ignored "-Wunused-label"
+#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
+#endif
+obj* initialize_init_lean_eqncompiler_matchpattern(obj*);
+static bool _G_initialized = false;
+obj* initialize_init_lean_eqncompiler_default(obj* w) {
+if (_G_initialized) return w;
+_G_initialized = true;
+if (io_result_is_error(w)) return w;
+w = initialize_init_lean_eqncompiler_matchpattern(w);
+if (io_result_is_error(w)) return w;
+return w;
+}

src/stage0/init/lean/eqncompiler/matchpattern.cpp

@@ -0,0 +1,152 @@
+// Lean compiler output
+// Module: init.lean.eqncompiler.matchpattern
+// Imports: init.lean.attributes
+#include "runtime/object.h"
+#include "runtime/apply.h"
+typedef lean::object obj;    typedef lean::usize  usize;
+typedef lean::uint8  uint8;  typedef lean::uint16 uint16;
+typedef lean::uint32 uint32; typedef lean::uint64 uint64;
+#if defined(__clang__)
+#pragma clang diagnostic ignored "-Wunused-parameter"
+#pragma clang diagnostic ignored "-Wunused-label"
+#elif defined(__GNUC__) && !defined(__CLANG__)
+#pragma GCC diagnostic ignored "-Wunused-parameter"
+#pragma GCC diagnostic ignored "-Wunused-label"
+#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
+#endif
+namespace lean {
+uint8 has_match_pattern_attribute_core(obj*, obj*);
+}
+obj* l_Lean_AttributeImpl_inhabited___lambda__4___boxed(obj*, obj*, obj*);
+obj* l_Lean_EqnCompiler_matchPatternAttr;
+obj* l_Lean_EqnCompiler_mkMatchPatternAttr___closed__3;
+obj* l_Lean_AttributeImpl_inhabited___lambda__3___boxed(obj*, obj*, obj*, obj*);
+obj* l_Lean_EqnCompiler_mkMatchPatternAttr(obj*);
+obj* l_Lean_PersistentEnvExtension_inhabited___rarg___lambda__1___boxed(obj*);
+obj* l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___closed__1;
+obj* l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___boxed(obj*, obj*);
+obj* l_Array_mkEmpty(obj*, obj*);
+obj* l_Lean_registerTagAttribute(obj*, obj*, obj*, obj*);
+obj* l_Lean_AttributeImpl_inhabited___lambda__5(obj*, obj*);
+obj* l_Lean_EqnCompiler_hasMatchPatternAttribute___boxed(obj*, obj*);
+obj* l_Lean_AttributeImpl_inhabited___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*);
+extern "C" obj* lean_name_mk_string(obj*, obj*);
+obj* l_ExceptT_Monad___rarg___lambda__8___boxed(obj*, obj*);
+uint8 l_Lean_TagAttribute_hasTag(obj*, obj*, obj*);
+obj* l_Lean_PersistentEnvExtension_inhabited___rarg___lambda__2___boxed(obj*);
+obj* l_Lean_AttributeImpl_inhabited___lambda__2___boxed(obj*, obj*, obj*, obj*);
+obj* l_Lean_EqnCompiler_mkMatchPatternAttr___closed__1;
+obj* l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1(obj*, obj*);
+obj* l_Lean_EqnCompiler_mkMatchPatternAttr___closed__2;
+obj* _init_l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___closed__1() {
+_start:
+{
+obj* x_1; obj* x_2; 
+x_1 = lean::box(0);
+x_2 = lean::alloc_cnstr(1, 1, 0);
+lean::cnstr_set(x_2, 0, x_1);
+return x_2;
+}
+}
+obj* l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___closed__1;
+return x_3;
+}
+}
+obj* _init_l_Lean_EqnCompiler_mkMatchPatternAttr___closed__1() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; 
+x_1 = lean::box(0);
+x_2 = lean::mk_string("matchPattern");
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+obj* _init_l_Lean_EqnCompiler_mkMatchPatternAttr___closed__2() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::mk_string("mark that a definition can be used in a pattern (remark: the dependent pattern matching compiler will unfold the definition)");
+return x_1;
+}
+}
+obj* _init_l_Lean_EqnCompiler_mkMatchPatternAttr___closed__3() {
+_start:
+{
+obj* x_1; 
+x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___boxed), 2, 0);
+return x_1;
+}
+}
+obj* l_Lean_EqnCompiler_mkMatchPatternAttr(obj* x_1) {
+_start:
+{
+obj* x_2; obj* x_3; obj* x_4; obj* x_5; 
+x_2 = l_Lean_EqnCompiler_mkMatchPatternAttr___closed__1;
+x_3 = l_Lean_EqnCompiler_mkMatchPatternAttr___closed__2;
+x_4 = l_Lean_EqnCompiler_mkMatchPatternAttr___closed__3;
+x_5 = l_Lean_registerTagAttribute(x_2, x_3, x_4, x_1);
+return x_5;
+}
+}
+obj* l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___boxed(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; 
+x_3 = l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1(x_1, x_2);
+lean::dec(x_2);
+lean::dec(x_1);
+return x_3;
+}
+}
+namespace lean {
+uint8 has_match_pattern_attribute_core(obj* x_1, obj* x_2) {
+_start:
+{
+obj* x_3; uint8 x_4; 
+x_3 = l_Lean_EqnCompiler_matchPatternAttr;
+x_4 = l_Lean_TagAttribute_hasTag(x_3, x_1, x_2);
+lean::dec(x_2);
+lean::dec(x_1);
+return x_4;
+}
+}
+}
+obj* l_Lean_EqnCompiler_hasMatchPatternAttribute___boxed(obj* x_1, obj* x_2) {
+_start:
+{
+uint8 x_3; obj* x_4; 
+x_3 = lean::has_match_pattern_attribute_core(x_1, x_2);
+x_4 = lean::box(x_3);
+return x_4;
+}
+}
+obj* initialize_init_lean_attributes(obj*);
+static bool _G_initialized = false;
+obj* initialize_init_lean_eqncompiler_matchpattern(obj* w) {
+if (_G_initialized) return w;
+_G_initialized = true;
+if (io_result_is_error(w)) return w;
+w = initialize_init_lean_attributes(w);
+if (io_result_is_error(w)) return w;
+l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___closed__1 = _init_l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___closed__1();
+lean::mark_persistent(l_Lean_EqnCompiler_mkMatchPatternAttr___lambda__1___closed__1);
+l_Lean_EqnCompiler_mkMatchPatternAttr___closed__1 = _init_l_Lean_EqnCompiler_mkMatchPatternAttr___closed__1();
+lean::mark_persistent(l_Lean_EqnCompiler_mkMatchPatternAttr___closed__1);
+l_Lean_EqnCompiler_mkMatchPatternAttr___closed__2 = _init_l_Lean_EqnCompiler_mkMatchPatternAttr___closed__2();
+lean::mark_persistent(l_Lean_EqnCompiler_mkMatchPatternAttr___closed__2);
+l_Lean_EqnCompiler_mkMatchPatternAttr___closed__3 = _init_l_Lean_EqnCompiler_mkMatchPatternAttr___closed__3();
+lean::mark_persistent(l_Lean_EqnCompiler_mkMatchPatternAttr___closed__3);
+REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "EqnCompiler"), "mkMatchPatternAttr"), 1, l_Lean_EqnCompiler_mkMatchPatternAttr);
+w = l_Lean_EqnCompiler_mkMatchPatternAttr(w);
+if (io_result_is_error(w)) return w;
+l_Lean_EqnCompiler_matchPatternAttr = io_result_get_value(w);
+lean::mark_persistent(l_Lean_EqnCompiler_matchPatternAttr);
+lean::register_constant(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "EqnCompiler"), "matchPatternAttr"), l_Lean_EqnCompiler_matchPatternAttr);
+REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "EqnCompiler"), "hasMatchPatternAttribute"), 2, l_Lean_EqnCompiler_hasMatchPatternAttribute___boxed);
+return w;
+}