From 8cdf44b87befb0b3407d745dc30ef26ec4d146b1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 1 Jul 2014 16:46:32 -0700
Subject: [PATCH] feat(frontends/lean/notation_cmd): allow 'max' to use as a
 precedence level

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/notation_cmd.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index 78fe19cc5..1c76dd829 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -183,7 +183,7 @@ static void parse_notation_local(parser & p, buffer<expr> & locals) {
 static action parse_action(parser & p, name const & prev_token, buffer<expr> & locals, buffer<token_entry> & new_tokens) {
     if (p.curr_is_token(g_colon)) {
         p.next();
-        if (p.curr_is_numeral()) {
+        if (p.curr_is_numeral() || p.curr_is_token_or_id(g_max)) {
             unsigned prec = parse_precedence(p, "invalid notation declaration, small numeral expected");
             return mk_expr_action(prec);
         } else if (p.curr_is_string()) {