michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/data/nat/find): rename 'choose' to 'find' to avoid conflict with combinatorics 'choose'

Browse source
This commit is contained in:
Jeremy Avigad 2015-07-25 12:28:39 -04:00
parent 43f5f70414
commit d3cd0bb8ff
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/data/nat/choose.lean → library/data/nat/find.lean
View file

@ -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