From 17f6ab3a710c33c99be9f583282c0eee1e4a4e1d Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sun, 3 Jan 2016 18:24:18 -0500 Subject: [PATCH] fix(library/data/set/basic): fix spacing in notation --- library/data/set/basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean index f7b2f9dc95..a8237cc330 100644 --- a/library/data/set/basic.lean +++ b/library/data/set/basic.lean @@ -563,14 +563,14 @@ section large_unions definition Union : set X := {x : X | ∃i, x ∈ b i} definition Inter : set X := {x : X | ∀i, x ∈ b i} - notation `⋃` binders, r:(scoped f, Union f) := r - notation `⋂` binders, r:(scoped f, Inter f) := r + notation `⋃` binders `, ` r:(scoped f, Union f) := r + notation `⋂` binders `, ` r:(scoped f, Inter f) := r definition bUnion : set X := {x : X | ∃₀ i ∈ a, x ∈ b i} definition bInter : set X := {x : X | ∀₀ i ∈ a, x ∈ b i} - notation `⋃` binders `∈` s, r:(scoped f, bUnion s f) := r - notation `⋂` binders `∈` s, r:(scoped f, bInter s f) := r + notation `⋃` binders ` ∈ ` s `, ` r:(scoped f, bUnion s f) := r + notation `⋂` binders ` ∈ ` s `, ` r:(scoped f, bInter s f) := r end large_unions