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

fix(library/data/set/filter): adapt to change in complete_lattice structure

Browse source
This commit is contained in:
Jeremy Avigad 2015-08-09 22:36:04 -04:00
parent 305f72bf4f
commit d17f72eb7c
1 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
library/data/set/filter.lean
View file

@ -284,14 +284,14 @@ protected definition complete_lattice [reducible] : algebra.complete_lattice (fi
le_refl := weakens.refl, le_refl := weakens.refl,
le_trans := @weakens.trans A, le_trans := @weakens.trans A,
le_antisymm := @weakens.antisymm A, le_antisymm := @weakens.antisymm A,
inf := inf, -- inf := inf,
le_inf := @inf_refines A, -- le_inf := @inf_refines A,
inf_le_left := refines_inf_left, -- inf_le_left := refines_inf_left,
inf_le_right := refines_inf_right, -- inf_le_right := refines_inf_right,
sup := sup, -- sup := sup,
sup_le := @refines_sup A, -- sup_le := @refines_sup A,
le_sup_left := sup_refines_left, -- le_sup_left := sup_refines_left,
le_sup_right := sup_refines_right, -- le_sup_right := sup_refines_right,
Inf := Inf, Inf := Inf,
Inf_le := @refines_Inf A, Inf_le := @refines_Inf A,
le_Inf := @Inf_refines A le_Inf := @Inf_refines A