diff --git a/library/init/lean/parser/declaration.lean b/library/init/lean/parser/declaration.lean index 38e3bbfb2b..cbc3c331eb 100644 --- a/library/init/lean/parser/declaration.lean +++ b/library/init/lean/parser/declaration.lean @@ -48,10 +48,10 @@ set_option class.instance_max_depth 300 def decl_modifiers.parser : command_parser := node! decl_modifiers [ doc_comment: doc_comment.parser?, + attrs: decl_attributes.parser?, visibility: node_choice! visibility {"private", "protected"}?, «noncomputable»: (symbol "noncomputable")?, «meta»: (symbol "meta")?, - attrs: decl_attributes.parser? ] @[derive has_tokens has_view]