feat(frontends/lean): increase binding power of ! and @

Remark: I did not add the constant "app".
Reason: It would break the standard library in many places.
Moreover, the current "max" is not just the binding power of
application, but also the binding power of identifiers, (, [, ...
It would be weird to call it "app"

closes #388

src/frontends/lean/builtin_exprs.cpp

@@ -428,7 +428,7 @@ static expr parse_overwrite_notation(parser & p, unsigned, expr const *, pos_inf
 }
 
 static expr parse_explicit_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
-    expr e = p.parse_expr(get_max_prec());
+    expr e = p.parse_expr(get_Max_prec());
     if (is_choice(e)) {
         buffer<expr> new_choices;
         for (unsigned i = 0; i < get_num_choices(e); i++)
@@ -440,7 +440,7 @@ static expr parse_explicit_expr(parser & p, unsigned, expr const *, pos_info con
 }
 
 static expr parse_consume_args_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
-    expr e = p.parse_expr(get_max_prec());
+    expr e = p.parse_expr(get_Max_prec());
     if (is_choice(e)) {
         buffer<expr> new_choices;
         for (unsigned i = 0; i < get_num_choices(e); i++)

src/frontends/lean/token_table.cpp

@@ -13,9 +13,11 @@ namespace lean {
 static unsigned g_arrow_prec      = 25;
 static unsigned g_decreasing_prec = 100;
 static unsigned g_max_prec        = 1024;
+static unsigned g_Max_prec        = 1024*1024;
 static unsigned g_plus_prec       = 65;
 static unsigned g_cup_prec        = 60;
 unsigned get_max_prec() { return g_max_prec; }
+unsigned get_Max_prec() { return g_Max_prec; }
 unsigned get_arrow_prec() { return g_arrow_prec; }
 unsigned get_decreasing_prec() { return g_decreasing_prec; }
 token_table add_command_token(token_table const & s, char const * token) {

src/frontends/lean/token_table.h

@@ -16,7 +16,10 @@ Author: Leonardo de Moura
 #endif
 
 namespace lean {
+// User-level maximum precedence
 unsigned get_max_prec();
+// Internal maximum precedence used for @ and ! operators
+unsigned get_Max_prec();
 unsigned get_arrow_prec();
 unsigned get_decreasing_prec();
 class token_info {

tests/lean/run/prec_max.lean

@@ -0,0 +1,18 @@
+open nat
+
+reserve postfix ⁻¹:(max + 1)
+
+postfix ⁻¹ := eq.symm
+
+constant foo (a b : nat) : a + b = 0
+
+theorem tst1 (a b : nat) : 0 = a + b :=
+!foo⁻¹
+
+constant f {a b : nat} (h1 : 0 = a + b) (h2 : a = b) : a = 0 ∧ b = 0
+
+example (a b : nat) : a = 0 ∧ b = 0 :=
+f !foo⁻¹ sorry
+
+example (a b : nat) : a = 0 ∧ b = 0 :=
+f !foo⁻¹ sorry⁻¹