From d17f72eb7c413e13f2b06532abf23bd5817291a4 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sun, 9 Aug 2015 22:36:04 -0400 Subject: [PATCH] fix(library/data/set/filter): adapt to change in complete_lattice structure --- library/data/set/filter.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/library/data/set/filter.lean b/library/data/set/filter.lean index c23461c93..2b06a4e44 100644 --- a/library/data/set/filter.lean +++ b/library/data/set/filter.lean @@ -284,14 +284,14 @@ protected definition complete_lattice [reducible] : algebra.complete_lattice (fi le_refl := weakens.refl, le_trans := @weakens.trans A, le_antisymm := @weakens.antisymm A, - inf := inf, - le_inf := @inf_refines A, - inf_le_left := refines_inf_left, - inf_le_right := refines_inf_right, - sup := sup, - sup_le := @refines_sup A, - le_sup_left := sup_refines_left, - le_sup_right := sup_refines_right, +-- inf := inf, +-- le_inf := @inf_refines A, +-- inf_le_left := refines_inf_left, +-- inf_le_right := refines_inf_right, +-- sup := sup, +-- sup_le := @refines_sup A, +-- le_sup_left := sup_refines_left, +-- le_sup_right := sup_refines_right, Inf := Inf, Inf_le := @refines_Inf A, le_Inf := @Inf_refines A