michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/structure_cmd): mark structure as 'class' when [class] modifier is used

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-03 17:46:03 -08:00
parent b112f3c582
commit 9531203d9d
3 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/structure_cmd.cpp
View file

@ -35,6 +35,7 @@ Author: Leonardo de Moura
#include "frontends/lean/tokens.h" #include "frontends/lean/tokens.h"
#include "frontends/lean/elaborator_exception.h" #include "frontends/lean/elaborator_exception.h"
#include "frontends/lean/type_util.h" #include "frontends/lean/type_util.h"
#include "frontends/lean/class.h"
namespace lean { namespace lean {
static name * g_tmp_prefix = nullptr; static name * g_tmp_prefix = nullptr;
@ -558,6 +559,8 @@ struct structure_cmd_fn {
add_alias(m_name, false); add_alias(m_name, false);
add_alias(m_mk); add_alias(m_mk);
add_rec_alias(rec_name); 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) { void save_def_info(name const & n) {

9
tests/lean/struct_class.lean Normal file
View file

@ -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

2
tests/lean/struct_class.lean.expected.out Normal file
View file

@ -0,0 +1,2 @@
point : Type → Type → Type
point : Type → Type → Type