missing docs linter doesn't trigger on macro_rules

Stream: lean4

[Alok Singh]

The issue is that macro_rules isn't flagged by linter.missingDocs

set_option linter.missingDocs true
-- warns about no doc comment
syntax "a" : term

-- no warning
macro_rules
  | `(a) => `(2)

[Aaron Liu]

Is this a problem?

[Robin Arnez]

I don't think there is any way to access that doc comment, so why bother?