feat: add support for not-in in exists (#425)

leanprover-community · Dec 7, 2023 · c4ece13 · c4ece13
1 parent d2a16f5
commit c4ece13
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Std/Util/ExtendedBinder.lean b/Std/Util/ExtendedBinder.lean
@@ -138,3 +138,5 @@ binder_predicate x " < " y:term => `($x < $y)
 binder_predicate x " ≤ " y:term => `($x ≤ $y)
 /-- Declare `∃ x ≠ y, ...` as syntax for `∃ x, x ≠ y ∧ ...` -/
 binder_predicate x " ≠ " y:term => `($x ≠ $y)
+/-- Declare `∃ x ∉ y, ...` as syntax for `∃ x, x ∉ y ∧ ...` -/
+binder_predicate x " ∉ " y:term => `($x ∉ $y)