max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(frontends/lean/vm_elaborator): use attribute parsers

Browse source
This commit is contained in:
Sebastian Ullrich 2019-02-15 19:16:33 +01:00 • committed by Leonardo de Moura
parent a6ac98966a
commit d083f8457a
1 changed files with 1 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/frontends/lean/vm_elaborator.cpp
View file

@ -164,17 +164,7 @@ decl_attributes to_decl_attributes(environment const & env, expr const & e, bool
buffer<expr> args;
auto attr = get_app_args(e, args);
auto n = const_name(attr);
if (n == "recursor") {
list<unsigned> idxs;
for (int i = args.size() - 1; i >= 0; i--)
idxs = cons(lit_value(unwrap_pos(args[i])).get_nat().get_small_value() - 1, idxs);
attributes.set_attribute(env, n, attr_data_ptr(new indices_attribute_data(idxs)));
} else if (n == "extern") {
// TODO(Sebastian): implement in C++ or Lean
} else {
lean_assert(args.empty());
attributes.set_attribute(env, n);
}
attributes.set_attribute(env, n, get_attribute(env, n).parse_data(e));
}
return attributes;
}