From 9561e379c76a4320c4b3b453d6135f57d2995258 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Sun, 20 Sep 2015 19:54:46 -0400
Subject: [PATCH] fix(library/data/set/basic): make set_of reducible

---
 library/data/set/basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean
index fd66b1057..8bbf429e1 100644
--- a/library/data/set/basic.lean
+++ b/library/data/set/basic.lean
@@ -234,7 +234,7 @@ ext (take x, !or.right_distrib)
 /- set-builder notation -/
 
 -- {x : X | P}
-definition set_of (P : X → Prop) : set X := P
+definition set_of [reducible] (P : X → Prop) : set X := P
 notation `{` binder `|` r:(scoped:1 P, set_of P) `}` := r
 
 -- {x ∈ s | P}