feat(frontends/lean/decl_cmds): allow many constants to be set in the same attribute command

src/frontends/lean/decl_cmds.cpp

@@ -1007,11 +1007,19 @@ static environment omit_cmd(parser & p) {
 }
 
 static environment attribute_cmd_core(parser & p, bool persistent) {
+    buffer<name> ds;
     name d          = p.check_constant_next("invalid 'attribute' command, constant expected");
+    ds.push_back(d);
+    while (p.curr_is_identifier()) {
+        ds.push_back(p.check_constant_next("invalid 'attribute' command, constant expected"));
+    }
     bool decl_only  = false;
     decl_attributes attributes(decl_only);
     attributes.parse(p);
-    return attributes.apply(p.env(), p.ios(), d, persistent);
+    environment env = p.env();
+    for (name const & d : ds)
+        env = attributes.apply(env, p.ios(), d, persistent);
+    return env;
 }
 
 static environment attribute_cmd(parser & p) {

tests/lean/run/attrs.lean

@@ -0,0 +1,19 @@
+structure A : Type :=
+(a : nat)
+
+structure B : Type :=
+(a : nat)
+
+structure C : Type :=
+(a : nat)
+
+constant f : A → B
+constant g : B → C
+constant h : C → C
+constant a : A
+
+attribute f g [coercion]
+set_option pp.coercions true
+set_option pp.beta true
+
+check h a