From 325d590bd0d779febb151a9504c8fecf676555a2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 8 Aug 2016 08:16:31 -0700
Subject: [PATCH] fix(frontends/lean): add missing files

---
 src/frontends/lean/pattern_attribute.cpp | 21 +++++++++++++++++++++
 src/frontends/lean/pattern_attribute.h   | 13 +++++++++++++
 2 files changed, 34 insertions(+)
 create mode 100644 src/frontends/lean/pattern_attribute.cpp
 create mode 100644 src/frontends/lean/pattern_attribute.h

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();
+}