fix(library/init/logic.lean): if_true and if_false take instance as implicit instead of inst_implicit

library/init/logic.lean

@@ -817,11 +817,11 @@ lemma if_simp_congr {α : Type u} {b c : Prop} [dec_b : decidable b] {x y u v :
 @if_ctx_simp_congr α b c dec_b x y u v h_c (λ h, h_t) (λ h, h_e)
 
 @[simp]
-def if_true {α : Type u} (t e : α) : (if true then t else e) = t :=
+def if_true {α : Type u} {h : decidable true} (t e : α) : (@ite true h α t e) = t :=
 if_pos trivial
 
 @[simp]
-def if_false {α : Type u} (t e : α) : (if false then t else e) = e :=
+def if_false {α : Type u} {h : decidable false} (t e : α) : (@ite false h α t e) = e :=
 if_neg not_false
 
 lemma if_ctx_congr_prop {b c x y u v : Prop} [dec_b : decidable b] [dec_c : decidable c]

tests/lean/run/simp_if_true_false.lean

@@ -0,0 +1,2 @@
+example (m n p : ℕ) : ite (m = m) n p = n := by simp
+example (m n p : ℕ) : ite (m ≠ m) n p = p := by simp