chore: reintroduce ∅ as regular notation

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 : α)

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 }