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

fix(frontends/lean/structure_cmd): simplify structure names

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-13 14:18:02 -08:00
parent 628faa10eb
commit c291063f3a
2 changed files with 21 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -698,14 +698,19 @@ struct structure_cmd_fn {
add_rec_on_alias(name(m_name, "cases_on"));
}
void get_parent_names(buffer<name> & parent_names) {
for (expr const & parent : m_parents)
parent_names.push_back(const_name(get_app_fn(parent)));
// Return the parent names without namespace prefix
void get_truncated_parent_names(buffer<name> & parent_names) {
for (expr const & parent : m_parents) {
name n = const_name(get_app_fn(parent));
if (!n.is_atomic() && n.is_string())
n = name(n.get_string());
parent_names.push_back(n);
}
}
void mk_coercion_names(buffer<name> & coercion_names) {
buffer<name> parent_names;
get_parent_names(parent_names);
get_truncated_parent_names(parent_names);
name_set found;
name_map<unsigned> non_unique;
for (name const & n : parent_names) {

12
tests/lean/run/struc_names.lean Normal file
View file

@ -0,0 +1,12 @@
namespace foo
structure structA [class] :=
mk :: (a : nat)
structure structB [class] extends structA :=
mk :: (b : nat)
check @structA.a
check @structB.to_structA
end foo