From 99864bbb31a4e16576c85a2a22467b1712339361 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 6 May 2021 22:35:23 +0200
Subject: [PATCH] =?UTF-8?q?chore:=20reintroduce=20`=E2=88=85`=20as=20regul?=
 =?UTF-8?q?ar=20notation?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Init/Core.lean                  | 3 +++
 tests/lean/emptyc.lean.expected.out | 4 ++--
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 5fcae7e601..9c7b2cdcf3 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -110,6 +110,9 @@ infix:50 " ≈ "  => HasEquiv.Equiv
 class EmptyCollection (α : Type u) where
   emptyCollection : α
 
+notation "{" "}" => EmptyCollection.emptyCollection
+notation "∅"     => EmptyCollection.emptyCollection
+
 /- Remark: tasks have an efficient implementation in the runtime. -/
 structure Task (α : Type u) : Type u where
   pure :: (get : α)
diff --git a/tests/lean/emptyc.lean.expected.out b/tests/lean/emptyc.lean.expected.out
index 6a5904246f..3a730562fc 100644
--- a/tests/lean/emptyc.lean.expected.out
+++ b/tests/lean/emptyc.lean.expected.out
@@ -1,4 +1,4 @@
 emptyc.lean:19:0-19:2: error: ambiguous, possible interpretations 
-  { x := 0 }
+  ∅
   
-  EmptyCollection.emptyCollection
+  { x := 0 }