refactor(frontends/lean): Bool does not need to be a reserved keyword

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/builtin_exprs.cpp

@@ -95,7 +95,6 @@ parse_table init_nud_table() {
     action Binders(mk_binders_action());
     expr x0 = mk_var(0);
     parse_table r;
-    r = r.add({transition("Bool", Skip)}, mk_Bool());
     r = r.add({transition("_", mk_ext_action(parse_placeholder))}, x0);
     r = r.add({transition("(", Expr), transition(")", Skip)}, x0);
     r = r.add({transition("fun", Binders), transition(",", mk_scoped_expr_action(x0))}, x0);

src/frontends/lean/token_table.cpp

@@ -58,7 +58,7 @@ token_table init_token_table() {
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {".{", 0}, {"Type", g_max_prec},
          {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0},
-         {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"raw", 0}, {"Bool", g_max_prec},
+         {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"raw", 0},
          {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
 
     char const * commands[] = {"theorem", "axiom", "variable", "definition", "{axiom}", "{variable}", "[variable]",

src/tests/frontends/lean/scanner.cpp

@@ -129,7 +129,7 @@ static void tst2() {
     scan("x.name");
     scan("x.foo");
     check("x.name", {tk::Identifier});
-    check("fun (x : Bool), x", {tk::Keyword, tk::Keyword, tk::Identifier, tk::Keyword, tk::Keyword,
+    check("fun (x : Bool), x", {tk::Keyword, tk::Keyword, tk::Identifier, tk::Keyword, tk::Identifier,
                  tk::Keyword, tk::Keyword, tk::Identifier});
     check_name("x10", name("x10"));
     // check_name("x.10", name(name("x"), 10));
@@ -161,7 +161,7 @@ static void tst2() {
     scan("0..1");
     check("0..1", {tk::Numeral, tk::Keyword, tk::Keyword, tk::Numeral});
     scan("theorem a : Bool axiom b : Int");
-    check("theorem a : Bool axiom b : Int", {tk::CommandKeyword, tk::Identifier, tk::Keyword, tk::Keyword,
+    check("theorem a : Bool axiom b : Int", {tk::CommandKeyword, tk::Identifier, tk::Keyword, tk::Identifier,
                 tk::CommandKeyword, tk::Identifier, tk::Keyword, tk::Identifier});
     scan("foo \"ttk\\\"\" : Int");
     check("foo \"ttk\\\"\" : Int", {tk::Identifier, tk::String, tk::Keyword, tk::Identifier});

tests/lean/run/simple.lean

@@ -1,3 +1,4 @@
+abbreviation Bool : Type.{1} := Type.{0}
 section
   parameter A : Type
 

tests/lean/run/t1.lean

@@ -1,3 +1,4 @@
+definition Bool : Type.{1} := Type.{0}
 print raw ((Bool))
 print raw Bool
 print raw fun (x y : Bool), x x

tests/lean/t4.lean

@@ -1,3 +1,4 @@
+definition [inline] Bool : Type.{1} := Type.{0}
 variable N : Type.{1}
 check N
 variable a : N

tests/lean/t4.lean.expected.out

@@ -8,7 +8,7 @@ len.{1} : Pi (A : Type) (n : N) (v : vec.{1} A n), N
 B -> B : Bool
 A -> A : Type.{l_1}
 C : Type.{l_2}
-t4.lean:24:6: error: unknown identifier 'A'
+t4.lean:25:6: error: unknown identifier 'A'
 R.{1 0} : Type -> Bool
 fun (x : N) (y : N), x : N -> N -> N
 choice N tst.N
@@ -18,7 +18,7 @@ foo.M
 tst.M : Type.{2}
 foo.M : Type.{3}
 foo.M : Type.{3}
-t4.lean:47:6: error: unknown identifier 'M'
+t4.lean:48:6: error: unknown identifier 'M'
 ok
 Declarations:
 tst.M
@@ -31,4 +31,5 @@ len
 vec
 f
 foo.M
+Bool
 -------------

tests/lean/t6.lean

@@ -1,3 +1,4 @@
+definition Bool : Type.{1} := Type.{0}
 section
   {parameter} A : Type  -- Mark A as implicit parameter
   parameter   R : A → A → Bool

tests/lean/t7.lean

@@ -1,3 +1,4 @@
+definition Bool : Type.{1} := Type.{0}
 variable and : Bool → Bool → Bool
 section
   {parameter} A : Type  -- Mark A as implicit parameter

tests/lean/t7.lean.expected.out

@@ -2,4 +2,4 @@ id.{2} : Pi {A : Type.{2}} (a : A), A
 trans.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool
 symm.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool
 equivalence.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool
-fun {A : Type.{l_1}} (R : A -> A -> Bool), (and (and (private.2020036202.refl.{l_1} A R) (symm.{l_1} A R)) (trans.{l_1} A R))
+fun {A : Type.{l_1}} (R : A -> A -> Bool), (and (and (private.2595647076.refl.{l_1} A R) (symm.{l_1} A R)) (trans.{l_1} A R))