michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/data/set/basic): make set_of reducible

Browse source
This commit is contained in:
Jeremy Avigad 2015-09-20 19:54:46 -04:00
parent 28a5ca5809
commit 9561e379c7
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/data/set/basic.lean
View file

@ -234,7 +234,7 @@ ext (take x, !or.right_distrib)
/- set-builder notation -/ /- set-builder notation -/
-- {x : X | P} -- {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 notation `{` binder `|` r:(scoped:1 P, set_of P) `}` := r
-- {x ∈ s | P} -- {x ∈ s | P}