From daf53e4de2e2c9d121baf6c5ce2e94440c6d6288 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sat, 16 May 2015 17:49:59 +1000 Subject: [PATCH] fix(library/algebra/order.lean): rename decidable_eq to had_decidable_eq to avoid conflict --- library/algebra/order.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/algebra/order.lean b/library/algebra/order.lean index 2d9217112..c2643aa78 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -313,7 +313,7 @@ section (assume H2 : b < a, inr (not_le_of_lt H2)) (assume H2 : ¬ b < a, inl (le_of_not_lt H2))) - definition decidable_eq [instance] : decidable (a = b) := + definition has_decidable_eq [instance] : decidable (a = b) := by_cases (assume H : a ≤ b, by_cases