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

fix(frontends/lean/decl_attributes): remove mdata

Browse source
This commit is contained in:
Leonardo de Moura 2019-06-18 15:25:34 -07:00
parent 91821529c0
commit 2b453de299
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/decl_attributes.cpp
View file

@ -80,7 +80,10 @@ syntax decl_attributes::expr_to_syntax(expr const & e) {
buffer<expr> args;
get_app_args(e, args);
buffer<syntax> new_args;
for (expr const & arg : args) {
for (expr arg : args) {
while (is_mdata(arg)) {
arg = mdata_expr(arg);
}
if (is_constant(arg)) {
new_args.push_back(mk_syntax_ident(const_name(arg)));
} else if (is_lit(arg)) {