From 12571c92d800a28e948be3d1cf53af821531fcc2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Wed, 6 Jan 2016 16:20:38 +0100 Subject: [PATCH] refactor(library/algebra): explicit parameters also for fun instances --- library/algebra/complete_lattice.lean | 2 +- library/algebra/lattice.lean | 4 ++-- library/algebra/order.lean | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/library/algebra/complete_lattice.lean b/library/algebra/complete_lattice.lean index 8c81380473..0d2f233d6c 100644 --- a/library/algebra/complete_lattice.lean +++ b/library/algebra/complete_lattice.lean @@ -278,7 +278,7 @@ open eq.ops complete_lattice definition complete_lattice_fun [instance] (A B : Type) [complete_lattice B] : complete_lattice (A → B) := -⦃ complete_lattice, lattice_fun, +⦃ complete_lattice, lattice_fun A B, Inf := λS x, Inf ((λf, f x) ' S), le_Inf := take f S H x, le_Inf (take y Hy, obtain g `g ∈ S` `g x = y`, from Hy, `g x = y` ▸ H g `g ∈ S` x), diff --git a/library/algebra/lattice.lean b/library/algebra/lattice.lean index ad18c1d65e..f5a9022d14 100644 --- a/library/algebra/lattice.lean +++ b/library/algebra/lattice.lean @@ -121,8 +121,8 @@ definition lattice_Prop [instance] : lattice Prop := le_sup_right := @or.intro_right ⦄ -definition lattice_fun [instance] {A B : Type} [lattice B] : lattice (A → B) := -⦃ lattice, weak_order_fun, +definition lattice_fun [instance] (A B : Type) [lattice B] : lattice (A → B) := +⦃ lattice, weak_order_fun A B, inf := λf g x, inf (f x) (g x), le_inf := take f g h Hf Hg x, le_inf (Hf x) (Hg x), inf_le_left := take f g x, !inf_le_left, diff --git a/library/algebra/order.lean b/library/algebra/order.lean index 90d82c15e5..587450b7ee 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -445,7 +445,7 @@ definition weak_order_Prop [instance] : weak_order Prop := le_antisymm := λf g H1 H2, propext (and.intro H1 H2) ⦄ -definition weak_order_fun [instance] {A B : Type} [weak_order B] : weak_order (A → B) := +definition weak_order_fun [instance] (A B : Type) [weak_order B] : weak_order (A → B) := ⦃ weak_order, le := λx y, ∀b, x b ≤ y b, le_refl := λf b, !le.refl,