fix(frontends/lean/brackets): fix {(0,1)} (#415)

leanprover-community · Jul 28, 2020 · cbfee49 · cbfee49
1 parent 0c7d574
commit cbfee49
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 2 deletions.
diff --git a/src/frontends/lean/brackets.cpp b/src/frontends/lean/brackets.cpp
@@ -226,8 +226,14 @@ expr parse_curly_bracket(parser & p, unsigned, expr const *, pos_info const & po
         parser::local_scope scope(p);
         parser::all_id_local_scope scope_assumption(p);
         e = parse_lparen(p, 0, NULL, pos); // parses the `expr ')'` part of the expression
-        p.check_token_next(get_bar_tk(), "invalid set replacement notation, '|' expected");
-        return parse_set_replacement(p, pos, e);
+        if (p.curr_is_token(get_rcurly_tk())) {
+            // singleton `{ (...) }`
+            p.next();
+            return mk_singleton(p, pos, e);
+        } else {
+            p.check_token_next(get_bar_tk(), "invalid set replacement notation, '|' expected");
+            return parse_set_replacement(p, pos, e);
+        }
     } else if (p.curr_is_token(get_period_tk())) {
         p.next();
         p.check_token_next(get_rcurly_tk(), "invalid empty structure instance, '}' expected");

diff --git a/tests/lean/run/singleton_pair.lean b/tests/lean/run/singleton_pair.lean
@@ -0,0 +1,2 @@
+example : {(0,1)} = (singleton (0, 1) : set (ℕ × ℕ)) := rfl
+example : {(0,1)} = [(0,1)] := rfl