From 533ac2d5b292916b365efcf2ec5bd447c689823e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 2 Oct 2018 09:30:55 -0700 Subject: [PATCH] fix(library/init/lean/parser/declaration): attributes before visibility modifiers --- library/init/lean/parser/declaration.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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]