From d083f8457a0df5e14481ef3eefa35087d98a6236 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 15 Feb 2019 19:16:33 +0100 Subject: [PATCH] feat(frontends/lean/vm_elaborator): use attribute parsers --- src/frontends/lean/vm_elaborator.cpp | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/src/frontends/lean/vm_elaborator.cpp b/src/frontends/lean/vm_elaborator.cpp index a7fe38310a..fde1837e9a 100644 --- a/src/frontends/lean/vm_elaborator.cpp +++ b/src/frontends/lean/vm_elaborator.cpp @@ -164,17 +164,7 @@ decl_attributes to_decl_attributes(environment const & env, expr const & e, bool buffer args; auto attr = get_app_args(e, args); auto n = const_name(attr); - if (n == "recursor") { - list 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; }