fix(library/init/lean/parser/command): keywords in notation actions are not actual keywords

2018-09-12 15:07:54 -07:00 · 2018-09-12 15:07:54 -07:00 · a57573a5b7
commit a57573a5b7
parent b8dceda9b7
1 changed files with 3 additions and 3 deletions
--- a/library/init/lean/parser/command.lean
+++ b/library/init/lean/parser/command.lean
@ -81,9 +81,9 @@ node_choice! notation_symbol {
 def action.parser : command_parser :=
 node! action [":", action: node_choice! action_kind {
  prec: number,
-  "max",
-  "prev",
-  "scoped"
+  max: raw_symbol "max",
+  prev: raw_symbol "prev",
+  scoped: raw_symbol "scoped"
  /-TODO seq [
    "(",
    any_of ["foldl", "foldr"],