Use unicode not for mkSet_not_elem_of.

53edf58b · Robbert Krebbers · c7995ce7 · 53edf58b
Commit 53edf58b authored Feb 16, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

prelude/sets.v prelude/sets.v +1 -1

No files found.
--- a/prelude/sets.v
+++ b/prelude/sets.v
@@ -20,7 +20,7 @@ Proof. by split; [split | |]; repeat intro. Qed.

 Lemma mkSet_elem_of {A} (f : A → Prop) x : f x → x ∈ mkSet f.
 Proof. done. Qed.
-Lemma mkSet_not_elem_of {A} (f : A → Prop) x : ~f x → x ∉ mkSet f.
+Lemma mkSet_not_elem_of {A} (f : A → Prop) x : ¬f x → x ∉ mkSet f.
 Proof. done. Qed.

 Instance set_ret : MRet set := λ A (x : A), {[ x ]}.