diff --git a/src/frontends/lean/pattern_attribute.cpp b/src/frontends/lean/pattern_attribute.cpp
new file mode 100644
index 0000000000..9d76872829
--- /dev/null
+++ b/src/frontends/lean/pattern_attribute.cpp
@@ -0,0 +1,21 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/attribute_manager.h"
+
+namespace lean {
+bool has_pattern_attribute(environment const & env, name const & d) {
+    return has_attribute(env, "pattern", d);
+}
+
+void initialize_pattern_attribute() {
+    register_attribute(basic_attribute("pattern", "mark that a definition can be used in a pattern"
+                                       "(remark: the dependent pattern matching compiler will unfold the definition)"));
+}
+
+void finalize_pattern_attribute() {
+}
+}
diff --git a/src/frontends/lean/pattern_attribute.h b/src/frontends/lean/pattern_attribute.h
new file mode 100644
index 0000000000..1d81e3b112
--- /dev/null
+++ b/src/frontends/lean/pattern_attribute.h
@@ -0,0 +1,13 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/environment.h"
+namespace lean {
+bool has_pattern_attribute(environment const & env, name const & d);
+void initialize_pattern_attribute();
+void finalize_pattern_attribute();
+}