From d3cd0bb8ffafa05858ad91c311ad364a7917775a Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sat, 25 Jul 2015 12:28:39 -0400 Subject: [PATCH] refactor(library/data/nat/find): rename 'choose' to 'find' to avoid conflict with combinatorics 'choose' --- library/data/nat/{choose.lean => find.lean} | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) rename library/data/nat/{choose.lean => find.lean} (94%) diff --git a/library/data/nat/choose.lean b/library/data/nat/find.lean similarity index 94% rename from library/data/nat/choose.lean rename to library/data/nat/find.lean index f1bdc0906..5758882d8 100644 --- a/library/data/nat/choose.lean +++ b/library/data/nat/find.lean @@ -97,9 +97,9 @@ private definition find_x : {x : nat | p x} := @fix _ _ _ wf_gtb find.F 0 lbp_zero end find_x -protected definition choose {p : nat → Prop} [d : decidable_pred p] : (∃ x, p x) → nat := +protected definition find {p : nat → Prop} [d : decidable_pred p] : (∃ x, p x) → nat := assume h, elt_of (find_x h) -protected theorem choose_spec {p : nat → Prop} [d : decidable_pred p] (ex : ∃ x, p x) : p (nat.choose ex) := +protected theorem find_spec {p : nat → Prop} [d : decidable_pred p] (ex : ∃ x, p x) : p (nat.find ex) := has_property (find_x ex) end nat