Skip to content
Snippets Groups Projects
Commit 248bc07a authored by David Swasey's avatar David Swasey
Browse files

Rename `cogpick` to `coGpick` (oops).

parent 74649a4b
No related branches found
No related tags found
No related merge requests found
......@@ -134,13 +134,13 @@ Section infinite.
End infinite.
(** * Pick elements from infinite sets *)
Definition cogpick `{Countable A, Infinite A} (X : coGset A) : A :=
Definition coGpick `{Countable A, Infinite A} (X : coGset A) : A :=
fresh (match X with FinGSet _ => | CoFinGset X => X end).
Lemma cogpick_elem_of `{Countable A, Infinite A} X :
¬set_finite X cogpick X X.
Lemma coGpick_elem_of `{Countable A, Infinite A} X :
¬set_finite X coGpick X X.
Proof.
unfold cogpick. destruct X as [X|X]; rewrite coGset_finite_spec; simpl.
unfold coGpick. destruct X as [X|X]; rewrite coGset_finite_spec; simpl.
done. by intros _; apply is_fresh.
Qed.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment