refactor(library/algebra): explicit parameters also for fun instances

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),

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,

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,