From 2e121182de005ec6509563a7dc255e075996fa62 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 21 Nov 2014 11:49:31 -0800 Subject: [PATCH] refactor(library/logic/decidable): rename decidable_rel -> decidable_pred, and decidable_rel2 -> decidable_rel --- library/logic/decidable.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/logic/decidable.lean b/library/logic/decidable.lean index 012350597..3c19f0bca 100644 --- a/library/logic/decidable.lean +++ b/library/logic/decidable.lean @@ -91,9 +91,9 @@ namespace decidable rec_on H (λh, H3 h) (λh, H4 h) --this can be proven using dependent version of "by_cases" end decidable -definition decidable_rel {A : Type} (R : A → Prop) := Π (a : A), decidable (R a) -definition decidable_rel2 {A : Type} (R : A → A → Prop) := Π (a b : A), decidable (R a b) -definition decidable_eq (A : Type) := decidable_rel2 (@eq A) +definition decidable_pred {A : Type} (R : A → Prop) := Π (a : A), decidable (R a) +definition decidable_rel {A : Type} (R : A → A → Prop) := Π (a b : A), decidable (R a b) +definition decidable_eq (A : Type) := decidable_rel (@eq A) --empty cannot depend on decidable, so we prove this here protected definition empty.has_decidable_eq [instance] : decidable_eq empty :=