From 9531203d9dbef01399f3cee501793947bd2d10b6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 3 Nov 2014 17:46:03 -0800
Subject: [PATCH] feat(frontends/lean/structure_cmd): mark structure as 'class'
 when [class] modifier is used

---
 src/frontends/lean/structure_cmd.cpp      | 3 +++
 tests/lean/struct_class.lean              | 9 +++++++++
 tests/lean/struct_class.lean.expected.out | 2 ++
 3 files changed, 14 insertions(+)
 create mode 100644 tests/lean/struct_class.lean
 create mode 100644 tests/lean/struct_class.lean.expected.out

diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index e2df452e4..c40e52767 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -35,6 +35,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/elaborator_exception.h"
 #include "frontends/lean/type_util.h"
+#include "frontends/lean/class.h"
 
 namespace lean {
 static name * g_tmp_prefix = nullptr;
@@ -558,6 +559,8 @@ struct structure_cmd_fn {
         add_alias(m_name, false);
         add_alias(m_mk);
         add_rec_alias(rec_name);
+        if (m_modifiers.is_class())
+            m_env = add_class(m_env, m_name);
     }
 
     void save_def_info(name const & n) {
diff --git a/tests/lean/struct_class.lean b/tests/lean/struct_class.lean
new file mode 100644
index 000000000..40fa376d0
--- /dev/null
+++ b/tests/lean/struct_class.lean
@@ -0,0 +1,9 @@
+structure point [class] (A : Type) (B : Type) :=
+mk :: (x : A) (y : B)
+
+print classes
+
+structure point2 (A : Type) (B : Type) :=
+mk :: (x : A) (y : B)
+
+print classes
diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out
new file mode 100644
index 000000000..ad2a5f32b
--- /dev/null
+++ b/tests/lean/struct_class.lean.expected.out
@@ -0,0 +1,2 @@
+point : Type → Type → Type
+point : Type → Type → Type