feat(frontends/lean/token_table): add ASCII notation for anonymous constructor

src/frontends/lean/token_table.cpp

@@ -85,7 +85,7 @@ void init_token_table(token_table & t) {
          {"%%", g_max_prec}, {"()", g_max_prec}, {")", 0}, {"'", 0},
          {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"Type*", g_max_prec},
-         {"{|", g_max_prec}, {"|}", 0}, {"(:", g_max_prec}, {":)", 0},
+         {"(:", g_max_prec}, {":)", 0},
          {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
          {"//", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0},  {"with", 0}, {"...", 0}, {",", 0},
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0},
@@ -114,7 +114,7 @@ void init_token_table(token_table & t) {
 
     pair<char const *, char const *> aliases[] =
         {{"λ", "fun"}, {"assume", "fun"}, {"take", "fun"}, {"forall", "Pi"},
-         {"∀", "Pi"}, {"Π", "Pi"}, {nullptr, nullptr}};
+         {"∀", "Pi"}, {"Π", "Pi"}, {"(|", "⟨"}, {"|)", "⟩"}, {nullptr, nullptr}};
 
     pair<char const *, char const *> cmd_aliases[] =
         {{"lemma", "theorem"}, {"def", "definition"}, {"proposition", "theorem"}, {"premise", "variable"}, {"premises", "variables"},

tests/lean/run/exists_intro1.lean

@@ -1,4 +1,3 @@
-
 example : ∃ x : nat, x = x :=
 Exists.intro 0 rfl
 
@@ -26,6 +25,9 @@ lemma ex6 : ∃ x : nat, x = x :=
 lemma ex7 : ∃ x y z : nat, x = y + z :=
 ⟨1, 1, 0, rfl⟩
 
+lemma ex8 : ∃ x y z : nat, x = y + z :=
+(| 1, 1, 0, rfl |)
+
 example : ∃ x : nat, x = x :=
 ⟨0, rfl⟩
 

tests/lean/run/match_anonymous_constructor.lean

@@ -1,4 +1,3 @@
-
 definition p1 := (10, 20, 30)
 
 definition v2 : nat :=
@@ -7,3 +6,8 @@ match p1 with
 end
 
 example : v2 = 10 := rfl
+
+definition v3 : nat :=
+match p1 with
+(| a, b |) := a
+end

tests/lean/run/parent_struct_inst.lean

@@ -8,3 +8,5 @@ structure B extends A :=
 (Hf : f = 0)
 
 example : B := ⟨0, rfl⟩
+
+example : B := (| 0, rfl |)

tests/lean/run/struct_value.lean

@@ -33,6 +33,8 @@ check { point3d . x := 1, y := 2, z := 3 }
 
 check (⟨10, rfl⟩ : Σ x : nat, x = x)
 
+check ((| 10, rfl |) : Σ x : nat, x = x)
+
 check ({ fst := 10, snd := rfl } : Σ x : nat, x = x)
 
 definition f (a : nat) : Σ x : nat, x = x :=