From 5087f038891ff45eaa69fd1995261648c12fcf79 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 8 Sep 2014 09:01:29 -0700 Subject: [PATCH] refactor(library/logic/classes/decidable): rename 'decidable_eq_to_decidable' theorem to 'of_decidable_eq' --- library/logic/classes/decidable.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/logic/classes/decidable.lean b/library/logic/classes/decidable.lean index 14ca50d4dc..6705dd3561 100644 --- a/library/logic/classes/decidable.lean +++ b/library/logic/classes/decidable.lean @@ -99,7 +99,7 @@ end decidable inductive decidable_eq [class] (A : Type) : Type := intro : (Π x y : A, decidable (x = y)) → decidable_eq A -theorem decidable_eq_to_decidable [instance] {A : Type} (H : decidable_eq A) (x y : A) : decidable (x = y) := +theorem of_decidable_eq [instance] {A : Type} (H : decidable_eq A) (x y : A) : decidable (x = y) := decidable_eq.rec (λ H, H) H x y -coercion decidable_eq_to_decidable : decidable_eq +coercion of_decidable_eq : decidable_eq