register_simp_attr requires a docstring?

Stream: lean4

[François G. Dorais]

It looks like the register_simp_attr command now requires a docstring after the string description argument was dropped from the command syntax (a while ago on September 9). Is this intentional? It's not a bad idea to encourage good documentation but it caught me by surprise that it's _required_ in this case.

[Mario Carneiro]

it's because the string description argument is being taken from the doc string now

[Mario Carneiro]

that's a required argument, we just changed how you input it to make it easier to do long-form descriptions

[Mario Carneiro]

We could make the description optional though, just use "" or something

[François G. Dorais]

Ah! That makes sense. Making it optional seems like a good idea since it's pretty weird to require a comment as part of the syntax.