From c5cbe1cc2c9b06e9cfcc961b87b6ae9f58fe120b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Jul 2014 09:53:05 -0700 Subject: [PATCH] refactor(library/standard): rename bool_decidable to prop_decidable Signed-off-by: Leonardo de Moura --- library/standard/{bool_decidable.lean => prop_decidable.lean} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename library/standard/{bool_decidable.lean => prop_decidable.lean} (92%) diff --git a/library/standard/bool_decidable.lean b/library/standard/prop_decidable.lean similarity index 92% rename from library/standard/bool_decidable.lean rename to library/standard/prop_decidable.lean index 7ffae64e3..9c469d766 100644 --- a/library/standard/bool_decidable.lean +++ b/library/standard/prop_decidable.lean @@ -14,5 +14,5 @@ theorem inhabited_decidable [instance] (a : Prop) : inhabited (decidable a) -- Note that inhabited_decidable is marked as an instance, and it is silently used -- for synthesizing the implicit argument in the following 'epsilon' -theorem bool_decidable [instance] (a : Prop) : decidable a +theorem prop_decidable [instance] (a : Prop) : decidable a := epsilon (λ d, true)